startsection <#710#>subsection<#710#><#711#>2<#711#><#712#>@<#712#><#713#>12pt plus 2pt minus 2pt<#713#>
<#714#>12pt plus 2pt minus 2pt<#714#><#715#>setsizesubsize<#716#>12pt<#716#>xipt<B></B><#715#>*<#147#><DIV class="CENTER">Abstract</DIV><#147#>
<#148#><EM>Quantum logic is static, describing automata having uncertain states
but no state transitions and no Heisenberg uncertainty tradeoff. We
cast Girard's linear logic in the role of a dynamic quantum logic,
regarded as an extension of quantum logic with time nonstandardly
interpreted over a domain of linear automata and their dual linear
schedules. In this extension the uncertainty tradeoff emerges via the
``structure veil.'' When VLSI shrinks to where quantum effects are
felt, their computer-aided design systems may benefit from such logics
of computational behavior having a strong connection to quantum
mechanics.</EM><#148#>
<P>
startsection <#717#>section<#717#><#718#>1<#718#><#719#>@<#719#><#720#>24pt plus 2pt minus 2pt<#720#>
<#721#>12pt plus 2pt minus 2pt<#721#><#722#><FONT SIZE="+1"><B></B></FONT><#722#><#149#>Motivation<#149#>
<P>
VLSI designers will eventually need to reckon with quantum mechanics
(QM), certainly within 50 years and possibly by the 2010's.
Computer-aided design (CAD) tools will need to adapt accordingly.
<P>
Does this entail changing only the theory or also the logic of CAD
verification systems? That is, will it be enough just to change those
nonlogical axioms defining how electronics works, or will it prove
necessary to dig deeper and tamper with logic itself?
<P>
Birkhoff and von Neumann [#BN36#<tex2html_cite_mark>#1##<tex2html_cite_mark>#] incorporate quantum uncertainty
into Boolean logic by interpreting conjunction <I>A</I>∧<I>B</I> standardly
but modifying negation <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline3914#</SUP> to mean certainly not <I>A</I>, in the sense
that <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline3917#</SUP> holds in just those states having probability 0 of being
mistaken for a state in which <I>A</I> holds. This relationship of
unmistakability is an irreflexive symmetric binary relation on states
called <#151#><I>orthogonality</I><#151#> and denoted <I>x</I><tex2html_image_mark>#tex2html_wrap_inline3920#<I>y</I>. Disjunction as the
De Morgan dual of conjunction does not distribute over conjunction in
this <#152#><I>quantum logic</I><#152#> (QL), suggesting that the emergence of quantum
phenomena in VLSI will force changes to CAD verifiers at as fundamental
a level as their Boolean logic.
<P>
A set of states with such an orthogonality relation amounts to an
automaton with fuzzy states but without transitions. Hence this
quantum logic is a static logic expressing uncertainty but not
progress. In addition the uncertainty so represented is not full
Heisenberg uncertainty, in that it obeys no complementarity tradeoff.
And the logic is not a real logic in that it lacks an implication with
a deduction theorem or currying principle.
<P>
Quantum logic as a faithful abstraction of quantum mechanics must
necessarily be extendable to include these dynamic elements of time and
Heisenberg uncertainty. Time is standardly added to quantum logic in
terms of the group of automorphisms of the underlying ortholattice, and
from this one recovers Heisenberg uncertainty [#Var68#<tex2html_cite_mark>#1##<tex2html_cite_mark>#].
<P>
In this paper we raise the problem of formulating this extension as a
<#154#><I>language</I><#154#> extension. That is, what propositional logic of quantum
mechanics incorporates not only QM's uncertainty but also its central
dynamic qualities? While such a question would have had no precedent
in 1936, today we have a great variety of logics combining the elements
of truth and behavior [#Flo#<tex2html_cite_mark>#1##<tex2html_cite_mark>#,#Hoa69#<tex2html_cite_mark>#1##<tex2html_cite_mark>#,#Sal70#<tex2html_cite_mark>#1##<tex2html_cite_mark>#,#BR#<tex2html_cite_mark>#1##<tex2html_cite_mark>#,#Dij76#<tex2html_cite_mark>#1##<tex2html_cite_mark>#,#Pr76#<tex2html_cite_mark>#1##<tex2html_cite_mark>#,#Pn#<tex2html_cite_mark>#1##<tex2html_cite_mark>#], making
our problem a very reasonable one.
<P>
To indicate the form such an extension might take, we cast Girard's
linear logic [#Gir87#<tex2html_cite_mark>#1##<tex2html_cite_mark>#] as a ``generalized dynamic quantum logic.''
It is made dynamic by incorporating a temporal element. It is
generalized in that nonstandard notions of time are admitted. We give
several interpretations of linear logic that convey to varying degrees
the dynamic quality of the extension, relative to the base construed as
a static logic.
<P>
The model we find most evocative of physical behavior is that of a
restricted class of linear automata and their dual linear schedules,
state spaces and their dual event spaces. (Elsewhere we describe in
detail the yet more restricted class of chains as rigid local behaviors
[#Pr92e#<tex2html_cite_mark>#1##<tex2html_cite_mark>#].) In the section on measurement we anticipate a broader
class of linear automata, partial distributive lattices, but defer its
detailed treatment to another paper.
<P>
However the notion of time contemplated in this model is that of
computer science rather than physics, in that it is constituted as a
partial order rather than a group. Furthermore the complementary
parameters of time and information behave more symmetrically for linear
automata than do the corresponding complementary physical parameters of
time and energy for the Schrödinger wave equation. In the latter,
attributes are represented by (the eigenvectors of) operators on the
Hamiltonian, which denotes energy, whereas time parametrizes a group of
unitary operators <tex2html_verbatim_mark>#math40#<I>U</I>(<I>s</I> + <I>t</I>) = <I>U</I>(<I>s</I>)<I>U</I>(<I>t</I>) transforming Hilbert space and
acting as automorphisms of the underlying ortholattice.
<P>
But despite this departure from orthodox quantum mechanics we may
observe the quantum-like notions of complementarity and Heisenberg
uncertainty in linear automata. Our claim is that these are the
analogues for ordered time of the phenomena of those names encountered
in orthodox quantum mechanics. The corresponding mathematical basis
for the the respective complementarities is duality: Stone duality for
computer science, Pontrjagin duality for physics. We hope in the
future to formulate and apply dualities obtained from other metrics
such as real- or complex-valued distance [#CCMP#<tex2html_cite_mark>#1##<tex2html_cite_mark>#] to dynamic quantum
logic.
<P>
It is often asked ``how could anything real be like quantum
mechanics?'' A hybrid computational/quantum mechanics that substitutes
certain elements of perceived reality for quantum reality while
retaining the uncertainty tradeoff of standard quantum mechanics
creates a bridge between perceived reality and quantum reality that may
prove helpful in making this transition. Having such a hybrid might
make it easier for systems designers and physicists collaborating on
quantum CAD to talk to each other. And it may conceivably find some
application in the pedagogy of standard QM and elsewhere.
<P>
We leave as an open problem the interpretation of linear logic for
quantum mechanics with its standard notion of time. It seems clear
that we must replace the ordered monoid {0 ;SPMlt; 1} with the group of
complex numbers, with or without origin (the latter when viewed as a
multiplicative group), as the automaton and the schedule interpreting
linear logic's constant <tex2html_image_mark>#tex2html_wrap_inline3924#, and also as the ring of scalars over
which the spaces are defined. What is presently lacking is a
quantum-mechanically orthodox organization of the duality between the
temporal metric on events and the information (energy?) metric on
states.
<P>
To summarize, we extend static quantum logic to a richer dynamic
quantum logic, but modeled for computational rather than physical
processes. This gives computer science a quantum mechanics of its own,
while leaving open the question of whether orthodox quantum mechanics
can model linear logic along similar lines.
<P>
The rest of the paper is organized as follows. We start with quantum
logic as a conventional propositional logic with one of each
operation: conjunction, negation, disjunction, and give the semantics
making it the logic of an orthomodular lattice. We then present linear
logic as the extension of quantum logic, construed as a <#159#><I>static</I><#159#>
logic, with a second <#160#><I>dynamic</I><#160#> set of connectives, further endowed
with one implication for each set, along with a connective !<I>A</I>
coordinating the two sets. We then exhibit both of Girard's models of
linear logic: the nonconstructive quantum-logic-like phase space model
and the constructive coherence spaces model, preparing the reader for
the latter with a minitutorial in constructive logic. Next we describe
state spaces and their complementary event spaces, first as a model of
concurrent behavior, then as a constructive model of linear logic,
giving a sense in which linear logic is a logic of behavior. Finally
we describe the ``structure veil,'' interpreted as Heisenberg
uncertainty and illustrated with partial distributive lattices, the
details of which will appear in another paper.
<P>
startsection <#723#>section<#723#><#724#>1<#724#><#725#>@<#725#><#726#>24pt plus 2pt minus 2pt<#726#>
<#727#>12pt plus 2pt minus 2pt<#727#><#728#><FONT SIZE="+1"><B></B></FONT><#728#><#161#>Quantum Logic<#161#>
<P>
startsection <#729#>subsection<#729#><#730#>2<#730#><#731#>@<#731#><#732#>12pt plus 2pt minus 2pt<#732#>
<#733#>12pt plus 2pt minus 2pt<#733#><#734#>setsizesubsize<#735#>12pt<#735#>xipt<B></B><#734#><#162#>Static Logic<#162#>
<P>
Common to quantum and linear logic are the constants 0 and 1,
conjunction <I>A</I>∧<I>B</I>, disjunction <I>A</I>∨<I>B</I>, and negation <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline3929#</SUP>.
These are the constants and operations of a bounded lattice, satisfying
(i) 0 <tex2html_image_mark>#tex2html_wrap_inline3931# <I>A</I> and <I>A</I> <tex2html_image_mark>#tex2html_wrap_inline3933# 1; (ii) (<I>C</I> <tex2html_image_mark>#tex2html_wrap_inline3935# <I>A</I> and <I>C</I> <tex2html_image_mark>#tex2html_wrap_inline3937# <I>B</I>) iff
<I>B</I> <tex2html_image_mark>#tex2html_wrap_inline3945# <I>C</I>). For both these logics we require that negation,
<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline3947#</SUP>, be a <#163#><I>duality</I><#163#>: it must be (iv) <#164#><I>contravariant</I><#164#>:
<I>A</I> <tex2html_image_mark>#tex2html_wrap_inline3949# <I>B</I> iff <tex2html_verbatim_mark>#math43#<I>B</I><SUP><tex2html_image_mark>#tex2html_wrap_inline3951#</SUP> <tex2html_image_mark>#tex2html_wrap_inline3952# <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline3953#</SUP>, and (v) an <#165#><I>involution</I><#165#>:
The nonconstructive interpretation of these conditions is that a model
is a partially ordered set (<I>X</I>,≤), made an algebra with these
constants and operations, and with <I>A</I> <tex2html_image_mark>#tex2html_wrap_inline3959# <I>B</I> interpreted as <I>A</I>≤<I>B</I>. We will treat the constructive interpretation of the conditions
later.
<P>
We shall think of this logic as <#166#><I>static</I><#166#> in the sense that it talks
about states of affairs rather than about events of change. While the
apparently temporal proposition ``It is Tuesday'' is a legitimate atom
<I>P</I> of this logic, the validity of <tex2html_verbatim_mark>#math45#<I>P</I>∧<I>P</I> = <I>P</I> reveals its static
nature. In this logic asserting <I>P</I> twice does not make it any more
true. As we will see later, linear logic extends this static logic
with a dynamic conjunction ⊗ for which <tex2html_verbatim_mark>#math46#<I>A</I>⊗<I>A</I> does not in
general equal <I>A</I>.
<P>
startsection <#739#>subsection<#739#><#740#>2<#740#><#741#>@<#741#><#742#>12pt plus 2pt minus 2pt<#742#>
<#743#>12pt plus 2pt minus 2pt<#743#><#744#>setsizesubsize<#745#>12pt<#745#>xipt<B></B><#744#><#167#>Orthoframes and Ortholattices<#167#>
<P>
The following notions pervade both quantum and linear logic. A <#168#><I>Kripke structure</I><#168#> (<I>X</I>, <I>R</I>) consists of a set <I>X</I> of possible worlds or
<#169#><I>states</I><#169#> together with a binary relation <tex2html_verbatim_mark>#math47#<I>R</I>⊆<I>X</I><SUP>2</SUP> of <#170#><I>accessibility</I><#170#> between states. We identify each proposition about such
states with the set of states in which it holds. An <#171#><I>orthoframe</I><#171#>
[#Gol74#<tex2html_cite_mark>#1##<tex2html_cite_mark>#] is a Kripke structure (<I>X</I>,<tex2html_image_mark>#tex2html_wrap_inline3971#) where <tex2html_image_mark>#tex2html_wrap_inline3973# is a
symmetric irreflexive binary relation of <#173#><I>orthogonality</I><#173#> relating
pairs of states not mistakable for each other.
<P>
For any subset <tex2html_verbatim_mark>#math48#<I>Y</I>⊆<I>X</I> we define <I>Y</I><SUP><tex2html_image_mark>#tex2html_wrap_inline3976#</SUP> to be <tex2html_verbatim_mark>#math49#{<I>z</I> | ∀<I>y</I>∈<I>Y</I>[<I>z</I><tex2html_image_mark>#tex2html_wrap_inline3978#<I>y</I>]}, those states not mistakable for any state of <I>Y</I>.
A <tex2html_image_mark>#tex2html_wrap_inline3981#-<#174#><I>closed</I><#174#> subset <I>A</I> is one for which <I>A</I> = <I>Y</I><SUP><tex2html_image_mark>#tex2html_wrap_inline3984#</SUP> for some
<I>Y</I>. It may be verified that the <tex2html_image_mark>#tex2html_wrap_inline3987#-closed subsets <I>A</I> are just
those satisfying <tex2html_verbatim_mark>#math50#<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline3990#<tex2html_image_mark>#tex2html_wrap_inline3991#</SUP> = <I>A</I>; we take these for the propositions of
quantum logic. These are closed under arbitrary intersection and hence
form a complete lattice, with the join of a set of propositions being
the intersection of all propositions including them all. Moreover
<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline3993#</SUP> is both a duality (making <tex2html_verbatim_mark>#math51#<I>A</I> = <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline3995#<tex2html_image_mark>#tex2html_wrap_inline3996#</SUP> an alternative condition
to be <tex2html_image_mark>#tex2html_wrap_inline3998#-closed) and a complement, and satisfies the usual De
A lattice <tex2html_verbatim_mark>#math52#(<I>L</I>,∨, 0,∧, 1,<tex2html_image_mark>#tex2html_wrap_inline4000#) for which <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4002#</SUP> is a duality and
a complement is called an <#176#><I>ortholattice.</I><#176#> A <#177#><I>Boolean algebra</I><#177#>
is a distributive ortholattice, i.e. all non-Boolean ortholattices
necessarily fail distributivity.
<P>
startsection <#748#>subsection<#748#><#749#>2<#749#><#750#>@<#750#><#751#>12pt plus 2pt minus 2pt<#751#>
<#752#>12pt plus 2pt minus 2pt<#752#><#753#>setsizesubsize<#754#>12pt<#754#>xipt<B></B><#753#><#178#>Quantum Logic<#178#>
<P>
Quantum mechanics is based on a Hilbert space of states, a metrically
complete inner product space, made an orthoframe by interpreting
orthogonality standardly for Euclidean space. Although completeness
does not have a first-order definition for either inner product spaces
or orthoframes [#Gol84#<tex2html_cite_mark>#1##<tex2html_cite_mark>#], the condition of orthomodularity
[#BN36#<tex2html_cite_mark>#1##<tex2html_cite_mark>#] on the associated orthoframe does express completeness
exactly [#AA66#<tex2html_cite_mark>#1##<tex2html_cite_mark>#]. (Orthomodularity can be defined as either
<I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4004# <I>B</I> and <tex2html_verbatim_mark>#math53#<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4006#</SUP>∧<I>B</I> = 0 implies <I>A</I> = <I>B</I>, or
<tex2html_verbatim_mark>#math54#<I>A</I>∧(<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4009#</SUP>∨(<I>A</I>∧<I>B</I>)) <tex2html_image_mark>#tex2html_wrap_inline4010# <I>B</I>. The second ;SPMquot;ortho;SPMquot; in
;SPMquot;orthomodular ortholattice;SPMquot; can be dropped.)
<P>
Quantum logic is defined as the logic of orthomodular lattices. It is
a faithful abstraction of ``concrete'' QM, whose attributes are
projections of Hilbert space onto itself, hence subspaces of Hilbert
space.
<P>
Distributivity fails in the standard model. For simplicity consider
<I>R</I><SUP>3</SUP> instead of <tex2html_verbatim_mark>#math55#<tex2html_image_mark>#tex2html_wrap_inline4013#. Take <I>A</I> to be the <I>X</I>-axis and <I>B</I> to be a
diagonal on the <I>XY</I> plane. Then <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4019#</SUP> is the <I>YZ</I> plane, and
<tex2html_verbatim_mark>#math56#(<I>A</I>∨<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4022#</SUP>) = 1 while <I>A</I>∧<I>B</I> and <tex2html_verbatim_mark>#math57#<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4025#</SUP>∧<I>B</I> are both 0.
Hence <tex2html_verbatim_mark>#math58#(<I>A</I>∨<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4027#</SUP>)∧<I>B</I> = <I>B</I> while <tex2html_verbatim_mark>#math59#(<I>A</I>∧<I>B</I>)∨(<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4029#</SUP>∧<I>B</I>) = 0, a violation of distributivity. Birkhoff and von Neumann cite as
a physical example of the same breakdown of distributivity the case of
<I>A</I> and <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4032#</SUP> as the observations of a wave-function (a state in
<tex2html_verbatim_mark>#math60#<tex2html_image_mark>#tex2html_wrap_inline4034#) on one side or the other of some plane, and <I>B</I> the observation
of a wave-function in a symmetric state about that plane [#BN36#<tex2html_cite_mark>#1##<tex2html_cite_mark>#].
<P>
startsection <#757#>subsection<#757#><#758#>2<#758#><#759#>@<#759#><#760#>12pt plus 2pt minus 2pt<#760#>
<#761#>12pt plus 2pt minus 2pt<#761#><#762#>setsizesubsize<#763#>12pt<#763#>xipt<B></B><#762#><#183#>Limitations of Quantum Logic<#183#>
<P>
Quantum logic has been intensively studied in the intervening 56
years. A very recent bibliography of the subject lists 1851 papers
[#Pav92#<tex2html_cite_mark>#1##<tex2html_cite_mark>#]. Evidently this appealingly simple system has touched a
responsive chord with many philosophers of physics.
<P>
But quantum logic may be <#185#><I>too</I><#185#> abstract to be useful. First, it is
a very minimal logic of QM, not even addressing time, in particular
saying nothing about how wave functions evolve and how propositions may
change their values with time. Nor does Heisenberg uncertainty appear,
even implicitly; all that is represented is whether or not any two
given states are mistakable for each other.
<P>
Second, QL has no reasonable implication. Dalla Chiara [#Dch86#<tex2html_cite_mark>#1##<tex2html_cite_mark>#]
surveys a number of candidates for a quantum logic implication, all of
which are lacking in various ways. There does exist the well-known
<#187#><I>Sasaki hook</I><#187#> <tex2html_verbatim_mark>#math61#<I>A</I>→<I>B</I> = <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4037#</SUP>∨(<I>A</I>∧<I>B</I>), and Finch
[#Fin70#<tex2html_cite_mark>#1##<tex2html_cite_mark>#] has given a conjunction <tex2html_verbatim_mark>#math62#<I>A</I>.<I>B</I> = <I>A</I>∧(<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4039#</SUP>∨<I>B</I>) to go
with it satisfying <I>A</I>.1 = <I>A</I> = 1.<I>A</I>, <I>A</I>.0 = 0 = 0.<I>A</I> (i.e. <I>A</I>.<I>B</I> has the same
unit and annihilator as <I>A</I>∧<I>B</I>), <I>A</I>.<I>A</I> = <I>A</I> (idempotence), and
<tex2html_verbatim_mark>#math63#<I>A</I>.<I>B</I> <tex2html_image_mark>#tex2html_wrap_inline4046# <I>C</I> iff <tex2html_verbatim_mark>#math64#<I>B</I> <tex2html_image_mark>#tex2html_wrap_inline4048# <I>A</I>→<I>C</I>. However if A.B is associative,
commutative, or monotone in <I>A</I> [#RR91#<tex2html_cite_mark>#1##<tex2html_cite_mark>#, Prop. 1.2], or if there
exists an implication →<SUP>′</SUP> such that <tex2html_verbatim_mark>#math65#<I>A</I>.<I>B</I> <tex2html_image_mark>#tex2html_wrap_inline4053# <I>C</I> iff <tex2html_verbatim_mark>#math66#<I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4055# <I>B</I>→<SUP>′</SUP><I>C</I>, the lattice collapses to a Boolean algebra, showing that all
of those conditions are unsound for the standard model. Other
implications are similarly flawed.
<P>
These objections are overcome in the extension of quantum logic to
linear logic as a dynamic quantum logic.
<P>
One might also question whether the notions of duality and complement
should be conflated in the one operation. This rules out such models
of truth as chains with more than two truth values including fuzzy
logic, as well as our linear automata. This is not however a valid
objection to standard quantum logic, only to generalized quantum
logics, for which the natural duality may not be complementation.
<P>
A conceivable objection might be raised on the basis of Goldblatt's
observation that completeness of inner product spaces cannot be
expressed in the first-order language of orthoframes, witnessed by the
inner product subspace of countable-dimension Hilbert space <tex2html_verbatim_mark>#math67#<tex2html_image_mark>#tex2html_wrap_inline4058#
consisting of all ultimately zero sequences, which is incomplete but
elementarily equivalent to <tex2html_verbatim_mark>#math68#<tex2html_image_mark>#tex2html_wrap_inline4060# [#Gol84#<tex2html_cite_mark>#1##<tex2html_cite_mark>#]. We do not find this
objectionable either. Transitive closure of binary relations is
likewise not first-order expressible, yet this does not negate the
importance of being able to reason about transitive closure, a central
concern for both database managers and program verifiers. Instead both
first-order approximations (induction in Peano arithmetic) and exact
with transitive closure [#NT77#<tex2html_cite_mark>#1##<tex2html_cite_mark>#,#Ng84#<tex2html_cite_mark>#1##<tex2html_cite_mark>#]) have been proposed and used.
The same considerations should apply to orthomodularity, which has a
straightforward second-order definition which becomes not only first
order but an equation when expressed in the language of ortholattices.
<P>
startsection <#770#>section<#770#><#771#>1<#771#><#772#>@<#772#><#773#>24pt plus 2pt minus 2pt<#773#>
<#774#>12pt plus 2pt minus 2pt<#774#><#775#><FONT SIZE="+1"><B></B></FONT><#775#><#193#>Linear Logic<#193#>
<P>
startsection <#776#>subsection<#776#><#777#>2<#777#><#778#>@<#778#><#779#>12pt plus 2pt minus 2pt<#779#>
<#780#>12pt plus 2pt minus 2pt<#780#><#781#>setsizesubsize<#782#>12pt<#782#>xipt<B></B><#781#><#194#>Dynamic Connectives<#194#>
<P>
To the connectives of static or additive logic,<A NAME="tex2html2" HREF="footnode_mn.html#foot503" TARGET="footer"><SUP>2</SUP></A> linear logic adds a fifth, a static implication
<tex2html_verbatim_mark>#math69#<I>A</I>⇒<I>B</I>. Then to the resulting five items it adds a parallel set of
five more items, the <#196#><I>dynamic</I><#196#> or multiplicative connectives and
In addition there is a unary connective !<I>A</I> expressing static logic in
dynamic terms. We write <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4094#</SUP> for <tex2html_verbatim_mark>#math71#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4096#<tex2html_image_mark>#tex2html_wrap_inline4097#-9<I>mu</I><TT>o</TT><tex2html_image_mark>#tex2html_wrap_inline4098#, called linear
negation,<A NAME="tex2html3" HREF="footnode_mn.html#foot202" TARGET="footer"><SUP>3</SUP></A> and ?<I>A</I> for <tex2html_verbatim_mark>#math72#(!(<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4107#</SUP>))<SUP><tex2html_image_mark>#tex2html_wrap_inline4108#</SUP>, the De Morgan
dual of !<I>A</I>. This completes the language of linear logic.
<P>
The idempotence of <I>A</I>∧<I>A</I> and dually <I>A</I>∨<I>A</I> does not hold for
the dynamic connectives. Except for these, the dynamic logic on its
own behaves like the static logic. The conjunctions and disjunctions
are associative and commutative, and the four constants are the four
units of their associated connectives. However no distributivity laws
hold within each logic.
<P>
A full axiomatization of constructive linear logic is presented in
algebraic language in Section 3.5, to which readers preferring crisp
definitions are referred. Here we shall continue to convey the flavor
of linear logic in algebraically less demanding terms.
<P>
Thus far the only basis for differentiating the two logics is that
negation is defined with dynamic implication. A more fundamental
difference is that the dynamic logic draws distinctions that the static
does not. As the names ``static'' and ``dynamic'' suggest, these
distinctions can be thought of as motion-related. We shall shortly
give several formal interpretations of linear logic. To ease the
transition let us start with a relatively informal interpretation.
<P>
We view propositions as moving at various speeds. The dynamic logic
takes the motion into account to arrive at reliable conclusions. The
static logic ignores the motion, drawing its conclusions under the
assumption that all propositions are stationary. Some propositions are
indeed stationary, including all propositions !<I>A</I>, which we think of
as <I>A</I> halted or frozen, and for these static logic comes to the
correct conclusion. But for moving propositions dynamic logic reasons
that certain combinations, such as cars moving towards each other at
high speed, will combine messily, while static logic naively assumes no
damage.
<P>
Static logic's optimistic reasoning is formalized by the identity
<tex2html_verbatim_mark>#math73#!(<I>A</I>∧<I>B</I>) = !<I>A</I>⊗!<I>B</I>. That is, if frenetically moving <I>A</I> and <I>B</I>
are first optimistically combined <#203#><I>statically</I><#203#> (<I>A</I>∧<I>B</I>) and
then brought to a halt, the statically predicted effect is that of
halting <I>A</I> and <I>B</I> individually to yield !<I>A</I> and !<I>B</I>, and then using
dynamic reasoning to infer that these stationary objects will combine
harmlessly.
<P>
The constructive formalization of !<I>A</I> will later be seen to make
<tex2html_verbatim_mark>#math74#!<I>A</I> = <I>F</I>(<I>U</I>(<I>A</I>)), the Free dynamic object generated by the Underlying
static (intuitionistic or cartesian closed) structure of <I>A</I>. (In the
jargon, ! is a comonad on the category of dynamic behaviors having a
cartesian closed Eilenberg-Moore category of underlying or static
structures.)
<P>
The informal velocity metaphor does not convey all of the intuition, so
we supplement it with a second informal metaphor. Instead of calling
the static reasoner an optimist we will think of her as an angel, and
the dynamic reasoner as a mere mortal. To an angel everything
including mortals seems frozen in time, while to a mortal angels exist
only as an article of faith. Angels reason with static connectives,
mortals with dynamic.
<P>
The identity <tex2html_verbatim_mark>#math75#!(<I>A</I>∧<I>B</I>) = !<I>A</I>⊗!<I>B</I> presents a mortal view of an
angelic conjunction as a mortal conjunction. More secularly, we may
regard !<I>A</I> as an X-ray view of <I>A</I>, delivering a visible conjunction
of parts normally seen in conjunction only in the mind's (optimist's,
angel's) eye.
<P>
Although static implication can be considered defined by its Deduction
Theorem, we regard its real definition as <tex2html_verbatim_mark>#math76#<I>A</I>⇒<I>B</I> = !<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4129#<tex2html_image_mark>#tex2html_wrap_inline4130#-9<I>mu</I><TT>o</TT><I>B</I>. We view
dynamic <tex2html_verbatim_mark>#math77#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4132#<tex2html_image_mark>#tex2html_wrap_inline4133#-9<I>mu</I><TT>o</TT><I>B</I> as the <#204#><I>employment</I><#204#> of mortal <I>B</I> in the <#205#><I>observation</I><#205#> of experiment <I>A</I>. Thus <tex2html_verbatim_mark>#math78#<I>A</I>⇒<I>B</I> denotes <I>B</I> employed as
before but now equipped with an X-ray machine. This expansion of <I>B</I>'s
powers confers on <I>B</I> the vision of an angel.
<P>
We turn now to the more formal models of linear logic. We begin with
Girard's nonconstructive model, phase space, then treat constructive
logic in preparation for the constructive coherence spaces model.
<P>
startsection <#797#>subsection<#797#><#798#>2<#798#><#799#>@<#799#><#800#>12pt plus 2pt minus 2pt<#800#>
<#801#>12pt plus 2pt minus 2pt<#801#><#802#>setsizesubsize<#803#>12pt<#803#>xipt<B></B><#802#><#206#>Phase Space<#206#>
<P>
The linear logic of phase space is that of lattices with a duality
(ortholattices less the requirement that <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4141#</SUP> be a complement),
based on a not necessarily irreflexive orthoframe, and extended to talk
about a monoid structure, the dynamical component. Formally, a <#207#><I>phase space</I><#207#> <tex2html_verbatim_mark>#math79#(<I>X</I>, + ,<tex2html_image_mark>#tex2html_wrap_inline4143#,<tex2html_image_mark>#tex2html_wrap_inline4144#) is a commutative monoid <tex2html_verbatim_mark>#math80#(<I>X</I>, + ,<tex2html_image_mark>#tex2html_wrap_inline4146#)
(say the reals under addition) together with a subset <tex2html_verbatim_mark>#math81#<tex2html_image_mark>#tex2html_wrap_inline4148#⊆<I>X</I>, the unit of <tex2html_verbatim_mark>#math82#<tex2html_image_mark>#tex2html_wrap_inline4150#<I>em</I>, defining a binary relation <I>x</I><tex2html_image_mark>#tex2html_wrap_inline4152#<I>y</I> holding
just when <tex2html_verbatim_mark>#math83#<I>x</I> + <I>y</I>∈<tex2html_image_mark>#tex2html_wrap_inline4154#. We no longer require irreflexivity for
orthogonality, whence we cannot guarantee that <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4156#</SUP> will be a
complement.
<P>
The monoidal structure serves to define the dynamic connectives.
<tex2html_verbatim_mark>#math84#<I>A</I>⊗<I>B</I> is defined as <tex2html_verbatim_mark>#math85#{<I>a</I> + <I>b</I> | <I>a</I>∈<I>A</I>, <I>b</I>∈<I>B</I>}<SUP><tex2html_image_mark>#tex2html_wrap_inline4159#<tex2html_image_mark>#tex2html_wrap_inline4160#</SUP>, with De
Morgan dual <tex2html_verbatim_mark>#math86#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4162#<I>emB</I>. We take <tex2html_verbatim_mark>#math87#<tex2html_image_mark>#tex2html_wrap_inline4164# = <tex2html_image_mark>#tex2html_wrap_inline4165#. Dynamic
implication <tex2html_verbatim_mark>#math88#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4167#<tex2html_image_mark>#tex2html_wrap_inline4168#-9<I>mu</I><TT>o</TT><I>B</I> is given by <tex2html_verbatim_mark>#math89#<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4170#</SUP><tex2html_image_mark>#tex2html_wrap_inline4171#<I>emB</I>.
<P>
In this model think of a proposition as denoting a set of abstract
tasks, each identified with the quantity of say energy required for
it. Call two tasks <#210#><I>compatible</I><#210#> when the energy they consume
acting jointly sums to one of the quantities in the set <tex2html_image_mark>#tex2html_wrap_inline4173#, which
consists of all compatible such binary sums. Hence <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4175#</SUP> consists
of all quantities compatible with every quantity in <I>A</I>. <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4178#</SUP> is
contravariant: the bigger <I>A</I> gets the harder it becomes to belong to
<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4181#</SUP>. Now suppose <I>A</I> is a set of trains and <I>B</I> a set of stations
to be visited by those trains. Then <tex2html_verbatim_mark>#math90#<I>A</I>⊗<I>B</I> is the set of all
arrivals of trains at stations, each arrival identified with the
quantity of energy jointly expended by the train and the station on
that arrival. (Arrivals of the same joint energy will be coalesced.)
This set is then <tex2html_image_mark>#tex2html_wrap_inline4186#-closed to make it a proposition. The static
connectives serve merely to combine these sets logically, with
conjunction being interpreted standardly and disjunction being
nonstandard on account of the fuzziness created by nonorthogonality.
<P>
The operation !<I>A</I> is an <#211#><I>interior</I><#211#> operator, namely monotone
decreasing (<tex2html_verbatim_mark>#math92#!<I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4194# <I>A</I>). Its image (and also its fixpoints) are the
<#212#><I>open</I><#212#> or <#213#><I>free</I><#213#> sets. (These suffice to determine !<I>A</I>,
namely as the largest open set contained in <I>A</I>.)
<P>
Furthermore !<I>A</I> is a <#214#><I>dynamic-topological</I><#214#> interior, meaning that
<tex2html_verbatim_mark>#math93#!(<I>A</I>∧<I>B</I>) = !<I>A</I>⊗!<I>B</I> and !1 = <tex2html_image_mark>#tex2html_wrap_inline4200#. (Static-topological would
have meant ordinary topological interior, satisfying <tex2html_verbatim_mark>#math94#!(<I>A</I>∧<I>B</I>) = !<I>A</I>∧!<I>B</I> and !1 = 1. Traditional intuitionistic logic is
necessarily of this static kind since it lacks a separate dynamic
intersection distinct from static intersection, cf. Stone's topological
treatment of intuitionistic logic at the end of his paper
We define the dual notion of <#216#><I>closure</I><#216#>, ?<I>A</I>, as
<tex2html_verbatim_mark>#math95#(!(<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4205#</SUP>))<SUP><tex2html_image_mark>#tex2html_wrap_inline4206#</SUP>, and <#217#><I>static implication</I><#217#> <tex2html_verbatim_mark>#math96#<I>A</I>⇒<I>B</I> as <tex2html_verbatim_mark>#math97#!<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4209#<tex2html_image_mark>#tex2html_wrap_inline4210#-9<I>mu</I><TT>o</TT><I>B</I>.
<P>
We have seen that the language of linear logic is that of quantum logic
expanded with dynamic connectives and constants, and !<I>A</I> and ?<I>A</I>.
The laws of linear logic, at least those of its phase space model,
conservatively extend those of quantum logic less the axioms of
complementation (<tex2html_verbatim_mark>#math98#<I>A</I>∨<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4214#</SUP> = 1) and orthomodularity. <tex2html_verbatim_mark>#math99#<I>A</I>⊗<I>B</I>
is associative with <tex2html_image_mark>#tex2html_wrap_inline4217# as its unit. <tex2html_verbatim_mark>#math100#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4219#<I>emB</I> is the De
Morgan dual of <tex2html_verbatim_mark>#math101#<I>A</I>⊗<I>B</I>, and <tex2html_image_mark>#tex2html_wrap_inline4222# the negation of <tex2html_image_mark>#tex2html_wrap_inline4224#.
<P>
We have <tex2html_verbatim_mark>#math102#<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4226#</SUP> = <I>A</I><tex2html_image_mark>#tex2html_wrap_inline4227#<tex2html_image_mark>#tex2html_wrap_inline4228#-9<I>mu</I><TT>o</TT><tex2html_image_mark>#tex2html_wrap_inline4229#. Also <tex2html_verbatim_mark>#math103#(<I>A</I>⊗<I>B</I>)<tex2html_image_mark>#tex2html_wrap_inline4231#<tex2html_image_mark>#tex2html_wrap_inline4232#-9<I>mu</I><TT>o</TT><I>C</I> = <I>A</I><tex2html_image_mark>#tex2html_wrap_inline4233#<tex2html_image_mark>#tex2html_wrap_inline4234#-9<I>mu</I><TT>o</TT>(<I>B</I><tex2html_image_mark>#tex2html_wrap_inline4235#<tex2html_image_mark>#tex2html_wrap_inline4236#-9<I>mu</I><TT>o</TT><I>C</I>). Hence setting <I>C</I> = <tex2html_image_mark>#tex2html_wrap_inline4238# yields <tex2html_verbatim_mark>#math104#(<I>A</I>⊗<I>B</I>)<SUP><tex2html_image_mark>#tex2html_wrap_inline4240#</SUP> = <I>A</I><tex2html_image_mark>#tex2html_wrap_inline4241#<tex2html_image_mark>#tex2html_wrap_inline4242#-9<I>mu</I><TT>o</TT><I>B</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4243#</SUP>.
And we have two inference rules: from <tex2html_verbatim_mark>#math105#(!<I>A</I>)<SUP>n</SUP> <tex2html_image_mark>#tex2html_wrap_inline4245# <I>B</I> infer <tex2html_verbatim_mark>#math106#!<I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4247# <I>B</I>, and from <I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4249# <I>B</I> infer <tex2html_verbatim_mark>#math107#!<I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4251# <I>B</I>.
<P>
Characteristic properties of nonconstructive linear logic are <tex2html_verbatim_mark>#math108#<I>A</I>∨<I>A</I> = <I>A</I> = <I>A</I>∧<I>A</I>.
<P>
These are a representative but not complete list of properties of the
phase space model.
<P>
startsection <#832#>subsection<#832#><#833#>2<#833#><#834#>@<#834#><#835#>12pt plus 2pt minus 2pt<#835#>
<#836#>12pt plus 2pt minus 2pt<#836#><#837#>setsizesubsize<#838#>12pt<#838#>xipt<B></B><#837#><#218#>Constructive Logic<#218#>
<P>
So far both quantum logic and linear logic have been nonconstructive in
the sense that the models have been posets. Both Girard's coherence
spaces and our linear automata make the transition to <#219#><I>constructive
logic</I><#219#>, which we define here. Since few readers with an interest in
either hardware verification or quantum mechanics are likely to be
familiar with constructive logic, and since there are no really
accessible crash courses in the subject, we take the liberty of going
into some detail.
<P>
Whereas nonconstructive logic takes truth to be the purpose of
mathematics, constructive logic takes proof to be its practice. It is
the same with travel and communication. Existence of routes tells
whether you can get there, but when you need to get there you need a
particular route. Existence of a derivation or parse tree establishes
grammaticality, but when you need to understand you need a particular
phrase structure. Since physics treats the practice of the universe
rather than its purpose, physicists are likely to find constructive
logic more useful than nonconstructive.
<P>
Consider the nonconstructive definition of <I>A</I>∨<I>B</I> as the unique
binary operation on a poset satisfying the rule <tex2html_verbatim_mark>#math109#<I>A</I>∨<I>B</I> <tex2html_image_mark>#tex2html_wrap_inline4255# <I>C</I> iff
(<I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4257# <I>C</I> and <I>B</I> <tex2html_image_mark>#tex2html_wrap_inline4259# <I>C</I>). This definition treats <I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4261# <I>B</I> as
the fact <I>A</I>≤<I>B</I>, ``and'' as Boolean conjunction, and ``iff'' as
equality of truth values of such facts.
<P>
We adopt the constructive interpretation of <I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4264# <I>B</I> as a set of
proofs of <I>B</I> from <I>A</I> (called a <#220#><I>homset</I><#220#> <tex2html_verbatim_mark>#math110#<I>Hom</I>(<I>A</I>, <I>B</I>)). Proofs
<tex2html_verbatim_mark>#math111#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4269#<I>B</I> and <tex2html_verbatim_mark>#math112#<I>B</I><tex2html_image_mark>#tex2html_wrap_inline4271#<I>C</I> <#225#><I>compose</I><#225#> (the <#226#><I>cut rule</I><#226#>) to prove <tex2html_verbatim_mark>#math113#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4273#<I>C</I>, an associative operation.
And <I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4275# <I>A</I> always contains the trivial or identity proof of <I>A</I>
from itself. These conditions will be recognized as those defining a
<#229#><I>category</I><#229#> whose objects are propositions and whose morphisms are
proofs.
<P>
Continuing with the same example, we interpret ``and'' as cartesian
product of such homsets, and ``iff'' as a bijection between homsets.
The primary purpose of the bijection is not to serve as a constraint on
the interpretation of <I>A</I>∨<I>B</I> but to give a method for dealing with
conjunctions when they are encountered. However it does succeed in
constraining the interpretation indirectly, namely via the assumption
that the method will always be implementable.
<P>
The category of sets and binary relations supplies an example
interpretation of propositions and proofs, making <I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4279# <I>B</I> the
homset of all <tex2html_verbatim_mark>#math114#2<SUP>| B|×| A|</SUP> binary relations from <I>A</I> to <I>B</I>.
The right hand side of the rule, <tex2html_verbatim_mark>#math115#(<I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4284# <I>C</I>)×(<I>B</I> <tex2html_image_mark>#tex2html_wrap_inline4285# <I>C</I>), is
then the homset of all <tex2html_verbatim_mark>#math116#2<SUP>(| A|+| B|)×| C|</SUP> pairs <I>f</I>, <I>g</I> of
relations <tex2html_verbatim_mark>#math117#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4289#<I>C</I> and <tex2html_verbatim_mark>#math118#<I>B</I><tex2html_image_mark>#tex2html_wrap_inline4291#<I>C</I>. Then the
method will be implementable provided <I>A</I>∨<I>B</I> has been interpreted as
any set <I>D</I> of cardinality | <I>A</I>| + | <I>B</I>|, permitting the implementation of
a bijection between <I>D</I> <tex2html_image_mark>#tex2html_wrap_inline4296# <I>C</I> and <tex2html_verbatim_mark>#math119#(<I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4298# <I>C</I>)×(<I>B</I> <tex2html_image_mark>#tex2html_wrap_inline4299# <I>C</I>).
Such a bijection is called an <#236#><I>adjunction</I><#236#>.
<P>
This is just a local bijection for a single pair <I>A</I>, <I>B</I> of
propositions. We further require that the collection of all such
bijections of the logic be <#237#><I>natural</I><#237#> [#Mac#<tex2html_cite_mark>#1##<tex2html_cite_mark>#, p.16,p.77], a
global consistency condition whose effect is to force <I>D</I> to look like
the same juxtaposition or <#239#><I>disjoint sum</I><#239#> <I>A</I> + <I>B</I> to all such
bijections.
<P>
Now the rules and axioms of a constructive logic are not merely
conditions on the interpretation of connectives, but methods for
dealing with connectives. A corollary of this orientation is that the
above bijection must be regarded as a part of the logic: each different
choice of a bijection meeting these conditions determines a different
constructive logic. A constructive logic is thus like an algebra, with
proofs for elements and bijections between proofs for operations.
(Propositions <I>A</I> can participate here by being identified with the
trivial proof <tex2html_verbatim_mark>#math120#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4305#<I>A</I>.) The process of proving is
called <#242#><I>derivation</I><#242#>, and yields a particular proof.
<P>
This is not to say that the rules do not constrain. The connectives
must be interpreted so as to guarantee the implementability of the
methods. This constraint can be thought of as the nonconstructive
component of a constructive logic.
<P>
Returning to nonconstructively defined <I>A</I>∨<I>B</I>, it is possible to
derive associativity, <tex2html_verbatim_mark>#math121#(<I>A</I>∨<I>B</I>)∨<I>C</I> = <I>A</I>∨(<I>B</I>∨<I>C</I>), from the
definition, as the truth value 1. The corresponding constructive
situation is that we can derive <tex2html_verbatim_mark>#math122#(<I>A</I>∨<I>B</I>)∨<I>C</I>~≅~<I>A</I>∨(<I>B</I>∨<I>C</I>),
not as a truth value but as a certain isomorphism in some category.
<P>
Why the switch from equality to isomorphism? Our above
sets-and-relations example seemed on the surface to define <I>A</I>∨<I>B</I>
associatively, namely as juxtaposition or disjoint union <I>A</I> + <I>B</I>. The
trouble is, we cannot rely on those elements in <I>A</I>∩<I>B</I> to keep track
in <I>A</I>∨<I>B</I> of their respective origins, forcing us into some system
of marking to keep track. But such a system will typically mark
elements of <I>A</I> twice in <tex2html_verbatim_mark>#math123#(<I>A</I>∨<I>B</I>)∨<I>C</I> and only once in
<tex2html_verbatim_mark>#math124#<I>A</I>∨(<I>B</I>∨<I>C</I>), with the result that <tex2html_verbatim_mark>#math125#(<I>A</I>∨<I>B</I>)∨<I>C</I> = <I>A</I>∨(<I>B</I>∨<I>C</I>)
may fail. However the two sets <#243#><I>are</I><#243#> the same size, so at least we
can always put them in bijection. Furthermore there is a unique
``sensible'' bijection, namely what would be the identity if only we
could erase the marks without confusion. <#244#><I>This</I><#244#> bijection is the
isomorphism that we are able to derive constructively in the logic.
The bijection <tex2html_verbatim_mark>#math126#<I>A</I>∨<I>B</I> <tex2html_image_mark>#tex2html_wrap_inline4318# <I>C</I> iff (<I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4320# <I>C</I> and <I>B</I> <tex2html_image_mark>#tex2html_wrap_inline4322# <I>C</I>)
specified by our constructive logic uniquely determines the
associativity isomorphism. Furthermore the naturality of the bijection
guarantees the naturality of the isomorphism.
<P>
So what's the point of all this? Nonconstructive logic was easy, why
are we making it so complicated with naturality and isomorphisms and so
on?
<P>
In fact a nonconstructive reformulation of our constructive logic of
automata that captured its essence would be highly desirable. At
present we do not see how to do it. Meanwhile to take some of the edge
off the complexity of this constructivity we look on the bright side as
follows.
<P>
Constructive logic is object-oriented logic. A proposition is not an
abstraction outside the domain of discourse but an object inside the
domain. Much of modern mathematics consists of methods for
manipulating relations and functions between objects. By organizing
these methods into a calculus we obtain an attractive formal system.
And by drawing analogies with logic we make the rules of this system
seem more familiar---they become the familiar rules of traditional
logic or the not-so-familiar rules of constructive quantum logic.
<P>
startsection <#840#>subsection<#840#><#841#>2<#841#><#842#>@<#842#><#843#>12pt plus 2pt minus 2pt<#843#>
<#844#>12pt plus 2pt minus 2pt<#844#><#845#>setsizesubsize<#846#>12pt<#846#>xipt<B></B><#845#><#245#>Coherence Spaces<#245#>
<P>
So far our models have been single orthoframes, together with a monoid
in the case of phase space. Now we break up that one orthoframe into
many smaller orthoframes that we then take as our propositions. We
pass from nonconstructive to constructive linear logic by replacing the
inclusion between propositions <I>A</I>, <I>B</I> with a set <I>A</I> <tex2html_image_mark>#tex2html_wrap_inline4325# <I>B</I> of
``proofs'' of <I>B</I> from <I>A</I>.
<P>
A <#246#><I>coherence space</I><#246#> is an orthoframe (<I>X</I>,<tex2html_image_mark>#tex2html_wrap_inline4329#). (Girard calls
this a <#247#><I>web</I><#247#> and defines a coherence space to be the poset of the
coherent subsets of the web under inclusion.) We say that distinct
<I>x</I>, <I>y</I> are <#248#><I>coherent</I><#248#> when <I>x</I><tex2html_image_mark>#tex2html_wrap_inline4332#<I>y</I> and <#249#><I>incoherent</I><#249#>
otherwise. The <#250#><I>coherent subsets</I><#250#> are those <tex2html_verbatim_mark>#math127#<I>Y</I>⊆<I>X</I>
satisfying <tex2html_verbatim_mark>#math128#<I>Y</I><SUP>2</SUP> - <I>I</I>⊆<tex2html_image_mark>#tex2html_wrap_inline4335#: all distinct pairs in <I>Y</I> are
coherent. (Incoherence or <#251#><I>conflict</I><#251#> should be thought of here not
so much as partial interference as in quantum logic but as complete
incompatibility.)
<P>
A binary relation <I>R</I> from (<I>X</I>,<tex2html_image_mark>#tex2html_wrap_inline4339#) to (<I>Y</I>,<tex2html_image_mark>#tex2html_wrap_inline4341#) is <#252#><I>coherent</I><#252#>
when any two distinct <I>y</I>'s that <I>R</I> relates <I>x</I> to are coherent, and
<#253#><I>stable</I><#253#> when any two distinct <I>x</I>'s that the converse of <I>R</I>
relates <I>y</I> to are incoherent. The category <#254#><#847#><B>Coh</B><#847#><#254#> of coherence spaces
has all orthoframes for its objects, and for its maps from (<I>X</I>,<tex2html_image_mark>#tex2html_wrap_inline4349#)
to (<I>Y</I>,<tex2html_image_mark>#tex2html_wrap_inline4351#) all coherent stable binary relations <I>R</I> from <I>X</I> to
<I>Y</I>.
<P>
Define the <#255#><I>dual</I><#255#> of the orthoframe (<I>X</I>,<tex2html_image_mark>#tex2html_wrap_inline4356#) to be the orthoframe
(<I>X</I>,<tex2html_image_mark>#tex2html_wrap_inline4358#) obtained as <tex2html_verbatim_mark>#math129#<tex2html_image_mark>#tex2html_wrap_inline4360# = <I>X</I><SUP>2</SUP> - <I>I</I> - <tex2html_image_mark>#tex2html_wrap_inline4361#. In the dual, coherence and
incoherence are interchanged. If we dualize the objects of <#256#><#848#><B>Coh</B><#848#><#256#> and
also replace every binary relation by its transpose, we obtain a
category of orthoframes and their stable coherent binary relations once
again. Since no orthoframes or relations have been gained or lost, we
must have obtained <#257#><#849#><B>Coh</B><#849#><#257#> back again, but with its objects permuted.
We call the correspondence induced by this dualizing of objects and
reversing of arrows a <#258#><I>contravariant isomorphism</I><#258#> or <#259#><I>duality</I><#259#>
between <#260#><B>Coh</B><#260#> and itself. If we define the <#261#><I>opposite</I><#261#> of
<#262#><#850#><B>Coh</B><#850#><#262#>, written <#263#><#851#><B>Coh</B><#851#><#852#><SUP>op</SUP><#852#><#263#>, to be <#264#><#855#><B>Coh</B><#855#><#264#> with its edges reversed then we
can dispense with the adjective ``contravariant'' and say that this
duality is an <#265#><I>isomorphism</I><#265#> between <#266#><#856#><B>Coh</B><#856#><#266#> and <#267#><#857#><B>Coh</B><#857#><#858#><SUP>op</SUP><#858#><#267#>. (This
duality is harder to see with the linear stable function approach.)
<P>
We now give the coherence space interpretations of the operations of
linear logic. <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4365#</SUP> is the dual defined in the preceding
paragraph. <I>A</I>∨<I>B</I> is their disjoint union or juxtaposition. (Hence
if <I>A</I> has 3 elements and <I>B</I> 4 then <I>A</I>∨<I>B</I> has 7, and <tex2html_image_mark>#tex2html_wrap_inline4371# is
defined as for each of <I>A</I> and <I>B</I> separately, with <I>a</I><tex2html_image_mark>#tex2html_wrap_inline4375#<I>b</I> false for
any <I>a</I>∈<I>A</I> and <I>b</I>∈<I>B</I>.) <I>A</I>∧<I>B</I> is their cartesian product,
with <tex2html_verbatim_mark>#math130#(<I>a</I>, <I>b</I>)<tex2html_image_mark>#tex2html_wrap_inline4380#(<I>a'</I>, <I>b'</I>) just when <I>a</I><tex2html_image_mark>#tex2html_wrap_inline4382#<I>a'</I> and <I>b</I><tex2html_image_mark>#tex2html_wrap_inline4384#<I>b'</I>. This is
very much like vector spaces over {0, 1} but with vectors being
allowed to interfere (nonorthogonality).
<P>
The additives juxtapose spaces side by side, coherently for <I>A</I>∧<I>B</I>
and incoherently for <I>A</I>∨<I>B</I>, representing ``both'' or ``either''
respectively. The multiplicatives can be thought of as a more intimate
mixing consisting of the interactions of <I>A</I> and <I>B</I>: one interaction
for every pair (<I>a</I>, <I>b</I>) from <I>A</I>, <I>B</I> respectively, with pairs cohering
pairwise for <tex2html_verbatim_mark>#math131#<I>A</I>⊗<I>B</I> and dually for <tex2html_verbatim_mark>#math132#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4394#<I>emB</I>.
<P>
We take !<I>A</I> to consist of all <#268#><I>finite</I><#268#> coherent subsets of <I>A</I>,
with <I>Y</I><tex2html_image_mark>#tex2html_wrap_inline4398#<I>Z</I> just when <tex2html_verbatim_mark>#math133#<I>Y</I>×<I>Z</I>⊆<tex2html_image_mark>#tex2html_wrap_inline4400#, that is, every
element of <I>Y</I> coheres with every element of <I>Z</I>. The remaining
operations are defined standardly.
<P>
(In Girard's version of coherence spaces, the binary relations become
functions between coherence spaces. A binary relation from <I>X</I> to <I>Y</I>
can described as a function <I>f</I> : <I>X</I>→2<SUP>Y</SUP>. The functions corresponding
to coherent relations have only coherent subsets of <I>Y</I> in their image,
the set of which we can therefore substitute for 2<SUP>Y</SUP>. We can
linearly extend the domain of <I>f</I> to the coherent subsets of <I>X</I> by
defining <tex2html_verbatim_mark>#math134#<I>f</I> (<I>Z</I>) = <tex2html_image_mark>#tex2html_wrap_inline4411#<I>f</I> (<I>z</I>) at each coherent <tex2html_verbatim_mark>#math135#<I>Z</I>⊆<I>X</I>,
so that the extended <I>f</I> is a linear function between coherence
spaces. The functions corresponding to stable relations 2<SUP>Y</SUP> map
distinct coherent pairs to disjoint subsets of <I>Y</I>, so we call such
functions stable. Then <#270#><#865#><B>Coh</B><#865#><#270#> can equivalently be defined as the
category of coherence spaces defined in this way and the linear stable
functions between them.)
<P>
startsection <#866#>subsection<#866#><#867#>2<#867#><#868#>@<#868#><#869#>12pt plus 2pt minus 2pt<#869#>
<#870#>12pt plus 2pt minus 2pt<#870#><#871#>setsizesubsize<#872#>12pt<#872#>xipt<B></B><#871#><#271#>Algebraic Definition of Constructive Linear Logic<#271#>
<P>
Before going on to the next interpretation of linear logic, we shall
stop here to consider the essence of these constructive models.
Readers uncomfortable with categories may prefer to skip this section.
<P>
We understand classical propositional logic in terms of the class of
its models, namely Boolean algebras. These can be succinctly defined
as complemented distributive lattices.
<P>
Following Seely [#See89#<tex2html_cite_mark>#1##<tex2html_cite_mark>#] we may define linear logic analogously,
with constructivity calling for the substitution of categories for
algebras. A <#273#><I>constructive model of linear logic</I><#273#> consists of a
*-autonomous category <tex2html_verbatim_mark>#math136#<tex2html_image_mark>#tex2html_wrap_inline4417# with all finite products and a comonad !
with natural isomorphisms <tex2html_verbatim_mark>#math137#!(<I>A</I>×<I>B</I>)≅!<I>A</I>⊗!<I>B</I> and
A *-autonomous category [#Bar79#<tex2html_cite_mark>#1##<tex2html_cite_mark>#] is a representably self-dual
closed symmetric monoidal category <tex2html_verbatim_mark>#math139#<tex2html_image_mark>#tex2html_wrap_inline4422#. Monoidal means that there
exists a binary operation (functor) <tex2html_verbatim_mark>#math140#⊗ : <tex2html_image_mark>#tex2html_wrap_inline4424#<SUP>2</SUP>→<tex2html_image_mark>#tex2html_wrap_inline4425# and an object
<tex2html_image_mark>#tex2html_wrap_inline4427# of <tex2html_verbatim_mark>#math141#<tex2html_image_mark>#tex2html_wrap_inline4429# having <tex2html_verbatim_mark>#math142#<I>A</I>⊗(<I>B</I>⊗<I>C</I>)≅(<I>A</I>⊗<I>B</I>)⊗<I>C</I> and
<tex2html_verbatim_mark>#math143#<tex2html_image_mark>#tex2html_wrap_inline4432#⊗<I>A</I>≅<I>A</I>≅<I>A</I>⊗<tex2html_image_mark>#tex2html_wrap_inline4433#, satisfying certain <#275#><I>coherence</I><#275#> conditions [#Mac#<tex2html_cite_mark>#1##<tex2html_cite_mark>#, p.161]. Symmetric monoidal adds
<tex2html_verbatim_mark>#math144#<I>A</I>⊗<I>B</I> ≅ <tex2html_verbatim_mark>#math145#<I>B</I>⊗<I>A</I>. Closed means that there exist a functor
<tex2html_verbatim_mark>#math146#<tex2html_image_mark>#tex2html_wrap_inline4438#<tex2html_image_mark>#tex2html_wrap_inline4439#-9<I>mu</I><TT>o</TT>: <tex2html_image_mark>#tex2html_wrap_inline4440#<tex2html_image_mark>#tex2html_wrap_inline4441#×<tex2html_image_mark>#tex2html_wrap_inline4442#→<tex2html_image_mark>#tex2html_wrap_inline4443# having <tex2html_verbatim_mark>#math147#<I>A</I>⊗<I>B</I>~ <tex2html_image_mark>#tex2html_wrap_inline4445# ~<I>C</I> iff
<tex2html_verbatim_mark>#math148#<I>A</I>~ <tex2html_image_mark>#tex2html_wrap_inline4447# ~<I>B</I><tex2html_image_mark>#tex2html_wrap_inline4448#<tex2html_image_mark>#tex2html_wrap_inline4449#-9<I>mu</I><TT>o</TT><I>C</I> (the ``Deduction Theorem,'' aka Currying). (We say
``having'' rather than ``satisfying'' as a reminder that this is not
just a condition but a particular natural bijection.)
<P>
Self-dual means that there exists an isomorphism
<tex2html_verbatim_mark>#math149#-<SUP><tex2html_image_mark>#tex2html_wrap_inline4453#</SUP> : <tex2html_image_mark>#tex2html_wrap_inline4454#→<tex2html_image_mark>#tex2html_wrap_inline4455#<tex2html_image_mark>#tex2html_wrap_inline4456#. Representably self-dual adds the requirement
that <tex2html_verbatim_mark>#math150#<tex2html_image_mark>#tex2html_wrap_inline4458# contains an object <tex2html_image_mark>#tex2html_wrap_inline4460# with which we may define
This defines the multiplicative or dynamic part of the generic model of
linear logic. The other multiplicative connectives are defined as
<tex2html_verbatim_mark>#math152#<tex2html_image_mark>#tex2html_wrap_inline4467# = <tex2html_image_mark>#tex2html_wrap_inline4468# and <tex2html_verbatim_mark>#math153#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4470#<I>emB</I> = (<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4471#</SUP>⊗<I>B</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4472#</SUP>)<SUP><tex2html_image_mark>#tex2html_wrap_inline4473#</SUP> = <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4474#</SUP><tex2html_image_mark>#tex2html_wrap_inline4475#<tex2html_image_mark>#tex2html_wrap_inline4476#-9<I>mu</I><TT>o</TT><I>B</I>.
<P>
For the additive or static part, <tex2html_verbatim_mark>#math154#<tex2html_image_mark>#tex2html_wrap_inline4478# has all finite products,
specifically <I>A</I>∧<I>B</I> and the empty product 1. We define
<tex2html_verbatim_mark>#math155#<I>A</I>∨<I>B</I> = (<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4482#</SUP>∧<I>B</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4483#</SUP>)<SUP><tex2html_image_mark>#tex2html_wrap_inline4484#</SUP> and = 1<SUP><tex2html_image_mark>#tex2html_wrap_inline4486#</SUP>.
<P>
Finally, relating the dynamic and static parts, there exists a comonad
structure <tex2html_verbatim_mark>#math156#(!, <I>ε</I>, <I>δ</I>) on <tex2html_verbatim_mark>#math157#<tex2html_image_mark>#tex2html_wrap_inline4489# with natural isomorphisms
<tex2html_verbatim_mark>#math158#!(<I>A</I>×<I>B</I>)≅!<I>A</I>⊗!<I>B</I> and <tex2html_verbatim_mark>#math159#!1≅<tex2html_image_mark>#tex2html_wrap_inline4492#. We may understand
this as a cartesian closed category <tex2html_verbatim_mark>#math160#<tex2html_image_mark>#tex2html_wrap_inline4494# and a functor <tex2html_verbatim_mark>#math161#<I>F</I> : <tex2html_image_mark>#tex2html_wrap_inline4496#→<tex2html_image_mark>#tex2html_wrap_inline4497# with
right adjoint <I>U</I> and with <tex2html_verbatim_mark>#math162#<I>F</I>(<I>A</I>∧<I>B</I>)≅<I>F</I>(<I>A</I>)⊗<I>F</I>(<I>B</I>) and
<tex2html_verbatim_mark>#math163#<I>F</I>(1)≅<tex2html_image_mark>#tex2html_wrap_inline4501#. The comonad is then <tex2html_verbatim_mark>#math164#(<I>FU</I>, <I>ε</I>, <I>FηU</I>)
where <I>η</I> and <I>ε</I> are the unit and counit of the adjunction,
with the further requirement that <tex2html_verbatim_mark>#math165#<tex2html_image_mark>#tex2html_wrap_inline4506# be recoverable as the
Eilenberg-Moore category of this comonad.
<P>
We define <tex2html_verbatim_mark>#math166#?<I>A</I> = (!(<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4508#</SUP>))<SUP><tex2html_image_mark>#tex2html_wrap_inline4509#</SUP> and <tex2html_verbatim_mark>#math167#<I>A</I>⇒<I>B</I> = !<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4511#<tex2html_image_mark>#tex2html_wrap_inline4512#-9<I>mu</I><TT>o</TT><I>B</I>.
<P>
This ends the category theory.
<P>
startsection <#917#>section<#917#><#918#>1<#918#><#919#>@<#919#><#920#>24pt plus 2pt minus 2pt<#920#>
<#921#>12pt plus 2pt minus 2pt<#921#><#922#><FONT SIZE="+1"><B></B></FONT><#922#><#278#>Linear Automata and Schedules<#278#>
<P>
We now describe a framework that is a cross between linear algebra and
automata theory, namely linear automata and their complementary linear
schedules. While this is not exactly quantum mechanics, its associated
logic is closer to quantum logic than either classical (Boolean) or
intuitionistic (Heyting) logic. And it offers internally consistent
accounts of time and measurement. We focus here on the special case of
linear automata as state spaces. In the section on measurement we will
mention briefly a more general class of linear automata based on
partial distributive lattices, to be dealt with in more detail in a
forthcoming paper.
<P>
startsection <#923#>subsection<#923#><#924#>2<#924#><#925#>@<#925#><#926#>12pt plus 2pt minus 2pt<#926#>
<#927#>12pt plus 2pt minus 2pt<#927#><#928#>setsizesubsize<#929#>12pt<#929#>xipt<B></B><#928#><#279#>State Spaces and Event Spaces<#279#>
<P>
If one thinks of a finite-dimensional vector space as populated with
column or ket vectors it is natural to think of its dual as consisting
of row or bra vectors of the same dimension. We define the notions of
state space and event space [#Pr91b#<tex2html_cite_mark>#1##<tex2html_cite_mark>#,#Pr92a#<tex2html_cite_mark>#1##<tex2html_cite_mark>#] in which events are to
states as bras are to kets. We thereby obtain a discrete yet linear
algebra of behaviors.
<P>
We read into the duality of events and states a
complementarity<A NAME="tex2html4" HREF="footnode_mn.html#foot281" TARGET="footer"><SUP>4</SUP></A> of time and information [#Pr92e#<tex2html_cite_mark>#1##<tex2html_cite_mark>#] analogous to that of
time and energy in mechanics. That our mechanics is more quantum than
classical follows from a Heisenberg-like uncertainty principle found
naturally, i.e. without special provision, in our model. Such
uncertainty is a litmus test for quantum rather than classical behavior
in any phase-space-like situation such as the complementarity of
position and momentum.
<P>
The behavior of an automaton is to alternately wait in a <#283#><I>state</I><#283#>
and perform a transition or <#284#><I>event</I><#284#>. We may think of the state as
bearing information representing the ``knowledge'' of the automaton
when in that state, and the event as modifying that information. At
the same time we may think of the event as taking place at a moment in
time, and the state as modifying or whiling away time.
<P>
Thus states <#285#><I>bear</I><#285#> information and <#286#><I>change</I><#286#> time, while
events <#287#><I>bear</I><#287#> time and <#288#><I>change</I><#288#> information.
<P>
We shall express this duality by giving two complementary representations
of such information. A state space will be a set of states ordered by
information content, while an event space will be a set of events ordered by
time.
<P>
State spaces generalize bc-domains (Scott domains or bounded-complete
algebraic cpo's) [#Gun92#<tex2html_cite_mark>#1##<tex2html_cite_mark>#], while their complementary event spaces
generalize Winskel's event structures [#Win86#<tex2html_cite_mark>#1##<tex2html_cite_mark>#]. This particular
duality is one small fragment of Birkhoff-Stone duality
[#Bir33#<tex2html_cite_mark>#1##<tex2html_cite_mark>#,#Sto36#<tex2html_cite_mark>#1##<tex2html_cite_mark>#,#Sto37#<tex2html_cite_mark>#1##<tex2html_cite_mark>#,#Pri70#<tex2html_cite_mark>#1##<tex2html_cite_mark>#], with the partial distributive lattices
alluded to in the section on measurement constituting a much larger
fragment.
<P>
A state space can be thought of as a representation of behavior
somewhere in between a formal language as a set of traces and a
conventional state automaton. Loops of the latter are unrolled and
confluences are split apart. Forks (branch points) however are left
untouched as representing decisions, and a new kind of confluence
representing concurrency is introduced. The alphabet of symbols
labelling transitions to indicate what they do is omitted, permitting
us to focus on the underlying structure of computation.
<P>
Formally, a <#292#><I>state space</I><#292#> is a nonempty partially ordered set <I>X</I>
every nonempty subset <tex2html_verbatim_mark>#math168#<I>Y</I>⊆<I>X</I> of which has a meet or infimum
<tex2html_verbatim_mark>#math169#<tex2html_image_mark>#tex2html_wrap_inline4518#<I>Y</I>. We refer to the state <tex2html_verbatim_mark>#math170#<tex2html_image_mark>#tex2html_wrap_inline4520#<I>Y</I> as the <#293#><I>branch</I><#293#>
for <I>Y</I>, the state from which one must make decisions about which
portion of <I>Y</I> to narrow down to. Noting that the branch <tex2html_verbatim_mark>#math171#<tex2html_image_mark>#tex2html_wrap_inline4524#<I>X</I>
for the whole space is the least element of <I>X</I>, we call this the <#294#><I>initial state</I><#294#> and abbreviate it to <I>q</I><SUB>0</SUB>
<P>
A state space is interpreted as an automaton by interpreting <I>x</I>≤<I>y</I>
as a transition from <I>x</I> to <I>y</I>, with the least element as the initial
state. Its maximal directed sets (those <I>Y</I> for which every pair of
elements of <I>Y</I> has an upper bound in <I>Y</I>) correspond to the
alternative paths. A state space that is a tree (no confluences) has
no concurrency and exhibits purely branching behavior, with a maximal
directed set being a chain. Conversely a directed state space has only
one alternative, the whole space, and represents purely concurrent
behavior (possibly temporally constrained). A finite Boolean algebra
with <I>n</I> atoms represents the concurrent and temporally unconstrained
execution of <I>n</I> events. A finite distributive lattice generalizes
this to events scheduled by a poset, where the events correspond to the
prime elements, those not the join of two incomparable elements, and
the order on the prime elements gives the temporal constraints.
Nondistributive lattices are to be regarded as quotients of
distributive lattices, i.e. certain states are identified or
synchronized.
<P>
We think of states as containers of knowledge. The intended
interpretation of <I>x</I>≤<I>y</I> is that <I>y</I> is a refinement of, or addition
to, the state of knowledge of <I>x</I>. For example in state <I>x</I> we may
know that we are in California and going very fast, while in state
<I>y</I>≥<I>x</I> we may know that we are crossing the Golden Gate at 65 mph.
<P>
The knowledge in the branch <tex2html_verbatim_mark>#math172#<tex2html_image_mark>#tex2html_wrap_inline4541#<I>Y</I> is the disjunction of
the knowledge at the states in <I>Y</I>. Equivalently, <tex2html_verbatim_mark>#math173#<tex2html_image_mark>#tex2html_wrap_inline4544#<I>Y</I> is
that state that knows as much as possible without knowing something
contradicting some state of <I>Y</I>.
<P>
An <#295#><I>event space</I><#295#> is a nonempty partially ordered set <I>X</I> every
nonempty subset <tex2html_verbatim_mark>#math174#<I>Y</I>⊆<I>X</I> of which has a join or supremum <tex2html_image_mark>#tex2html_wrap_inline4549#<I>Y</I>. We refer to <tex2html_image_mark>#tex2html_wrap_inline4551#<I>Y</I> as the <#296#><I>completion</I><#296#> of <I>Y</I>. Noting
that the completion <tex2html_image_mark>#tex2html_wrap_inline4554#<I>X</I> for the whole space is the greatest
element of <I>X</I>, we call this the <#297#><I>final event</I><#297#> and abbreviate it to
∞
<P>
We think of events as markers of time. The intended interpretation of
<I>x</I>≤<I>y</I> is that <I>x</I> precedes or is simultaneous with <I>y</I>.
<P>
Just as vector spaces may be transformed with linear transformations
that hold the origin fixed and preserve linear combinations, so may
state spaces be transformed with state space transformations. A <#298#><I>state map</I><#298#> <I>f</I> : <I>X</I>→<I>Y</I> is a function between two state spaces that
preserves the initial state and all branches. That is, <tex2html_verbatim_mark>#math175#<I>f</I> (<I>q</I><SUB>0</SUB>) = <I>q</I><SUB>0</SUB>,
and <tex2html_verbatim_mark>#math176#<I>f</I> (<tex2html_image_mark>#tex2html_wrap_inline4563#<I>Y</I>) = <tex2html_image_mark>#tex2html_wrap_inline4564#<I>f</I> (<I>Y</I>) where <I>f</I> (<I>Y</I>) denotes the image
<tex2html_verbatim_mark>#math177#{<I>f</I> (<I>y</I>) | <I>y</I>∈<I>Y</I>} of <I>Y</I> under <I>f</I>.
<P>
The initial state represents absolute rather than relative ignorance.
No transformation of a state space can change the status of <I>q</I><SUB>0</SUB>; in
particular no states can be added below or to one side of <I>q</I><SUB>0</SUB>, only
above. We may identify <I>q</I><SUB>0</SUB> with the state of the universe at the Big
Bang, namely complete ignorance of all facts. (Facts which are always
true are deemed to contain zero knowledge for this purpose: if 1 + 1 = 2
is a universal truth then it was known at the Big Bang.) In <I>q</I><SUB>0</SUB> no
events have happened yet.
<P>
We call the situation <tex2html_verbatim_mark>#math178#<tex2html_image_mark>#tex2html_wrap_inline4575#<I>Y</I> = <I>q</I><SUB>0</SUB> a <#299#><I>dilemma</I><#299#> or blind
choice. The basic dilemma is <tex2html_verbatim_mark>#math179#<tex2html_image_mark>#tex2html_wrap_inline4577# = 2<tex2html_image_mark>#tex2html_wrap_inline4578# = 1<tex2html_image_mark>#tex2html_wrap_inline4579# = <tex2html_image_mark>#tex2html_wrap_inline4580#<tex2html_image_mark>#tex2html_wrap_inline4581#<tex2html_image_mark>#tex2html_wrap_inline4582#<I>by</I>2<tex2html_image_mark>#tex2html_wrap_inline4583# = <tex2html_image_mark>#tex2html_wrap_inline4584#<tex2html_image_mark>#tex2html_wrap_inline4585#<tex2html_image_mark>#tex2html_wrap_inline4586#<I>by</I> - <tex2html_image_mark>#tex2html_wrap_inline4587#<tex2html_image_mark>#tex2html_wrap_inline4588#<tex2html_image_mark>#tex2html_wrap_inline4589#<I>by</I> - <tex2html_image_mark>#tex2html_wrap_inline4590#<tex2html_image_mark>#tex2html_wrap_inline4591#<tex2html_image_mark>#tex2html_wrap_inline4592#<I>by</I>5<tex2html_image_mark>#tex2html_wrap_inline4593#<tex2html_image_mark>#tex2html_wrap_inline4594#<I>by</I>1<tex2html_image_mark>#tex2html_wrap_inline4595# (horn-shaped) where <I>Y</I> consists
of the top two elements. We have no information in <I>q</I><SUB>0</SUB> yet we are
obliged to make a choice there.
<P>
The dual notion of <#300#><I>event map</I><#300#> <I>f</I> : <I>X</I>→<I>Y</I> is a function between two
event spaces that preserves the final event and all completions.
<P>
The final event ∞ is as absolute as the initial state, for
similar reasons. For every state <I>q</I>, ∞ has not happened in
<I>q</I>. (Compare this with: for every event <I>u</I>, <I>u</I> has not happened in
<I>q</I><SUB>0</SUB>.) That is, ∞ never happens.
<P>
Informally, the time of the completion <tex2html_image_mark>#tex2html_wrap_inline4608#<I>Y</I> is the supremum of
the times of completion of the events in <I>Y</I>. Equivalently, <tex2html_image_mark>#tex2html_wrap_inline4611#<I>Y</I> is that event that is as early as possible while still following
every event of <I>Y</I>.
<P>
We call the situation <tex2html_verbatim_mark>#math180#<tex2html_image_mark>#tex2html_wrap_inline4614#<I>Y</I> = ∞ a <#301#><I>conflict</I><#301#>, dual to
dilemma. The basic conflict is <tex2html_verbatim_mark>#math181#<tex2html_image_mark>#tex2html_wrap_inline4616# = 2<tex2html_image_mark>#tex2html_wrap_inline4617# = 1<tex2html_image_mark>#tex2html_wrap_inline4618# = <tex2html_image_mark>#tex2html_wrap_inline4619#<tex2html_image_mark>#tex2html_wrap_inline4620#<tex2html_image_mark>#tex2html_wrap_inline4621#<I>by</I>2<tex2html_image_mark>#tex2html_wrap_inline4622# = <tex2html_image_mark>#tex2html_wrap_inline4623#<tex2html_image_mark>#tex2html_wrap_inline4624#<tex2html_image_mark>#tex2html_wrap_inline4625#<I>by</I> - <tex2html_image_mark>#tex2html_wrap_inline4626#<tex2html_image_mark>#tex2html_wrap_inline4627#<tex2html_image_mark>#tex2html_wrap_inline4628#<I>by</I> - <tex2html_image_mark>#tex2html_wrap_inline4629#<tex2html_image_mark>#tex2html_wrap_inline4630#<tex2html_image_mark>#tex2html_wrap_inline4631#<I>by</I>5<tex2html_image_mark>#tex2html_wrap_inline4632#<tex2html_image_mark>#tex2html_wrap_inline4633#<I>by</I>1<tex2html_image_mark>#tex2html_wrap_inline4634# with <I>Y</I> the bottom two
elements. The completion of <I>Y</I> is the event that never happens, hence
not all of <I>Y</I> can complete.
<P>
startsection <#960#>subsection<#960#><#961#>2<#961#><#962#>@<#962#><#963#>12pt plus 2pt minus 2pt<#963#>
<#964#>12pt plus 2pt minus 2pt<#964#><#965#>setsizesubsize<#966#>12pt<#966#>xipt<B></B><#965#><#302#>State Space Interpretation of LL<#302#>
<P>
We return now to linear logic to interpret its propositions and
connectives formally for state and event spaces. In the following
section we then give the informal behavioral intuition behind this
interpretation. This language of sums and products of spaces is a
close cousin of Birkhoff's generalize arithmetic of posets
[#Birk42#<tex2html_cite_mark>#1##<tex2html_cite_mark>#], elaborated on elsewhere [#Pr92a#<tex2html_cite_mark>#1##<tex2html_cite_mark>#].
<P>
The <#305#><I>dual</I><#305#> <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4639#</SUP> of a state space <I>A</I> is obtained as the order
dual of <I>A</I> - {<I>q</I><SUB>0</SUB>} with <I>q</I><SUB>0</SUB> then added back in at the bottom. That
is, holding <I>q</I><SUB>0</SUB> fixed, turn the rest of <I>A</I> upside down. This
operation can be seen to interchange <tex2html_verbatim_mark>#math182#<tex2html_image_mark>#tex2html_wrap_inline4646# = 2<tex2html_image_mark>#tex2html_wrap_inline4647# = 2<tex2html_image_mark>#tex2html_wrap_inline4648# = <tex2html_image_mark>#tex2html_wrap_inline4649#<tex2html_image_mark>#tex2html_wrap_inline4650#<tex2html_image_mark>#tex2html_wrap_inline4651#<I>by</I>2<tex2html_image_mark>#tex2html_wrap_inline4652# = <tex2html_image_mark>#tex2html_wrap_inline4653#<tex2html_image_mark>#tex2html_wrap_inline4654#<tex2html_image_mark>#tex2html_wrap_inline4655#<I>by</I> - <tex2html_image_mark>#tex2html_wrap_inline4656#<tex2html_image_mark>#tex2html_wrap_inline4657#<tex2html_image_mark>#tex2html_wrap_inline4658#<I>by</I> - <tex2html_image_mark>#tex2html_wrap_inline4659#<tex2html_image_mark>#tex2html_wrap_inline4660#<tex2html_image_mark>#tex2html_wrap_inline4661#<I>by</I>5<tex2html_image_mark>#tex2html_wrap_inline4662#<tex2html_image_mark>#tex2html_wrap_inline4663#<I>by</I>1<tex2html_image_mark>#tex2html_wrap_inline4664# and <tex2html_verbatim_mark>#math183#<tex2html_image_mark>#tex2html_wrap_inline4666# = 2<tex2html_image_mark>#tex2html_wrap_inline4667# = 2<tex2html_image_mark>#tex2html_wrap_inline4668# = <tex2html_image_mark>#tex2html_wrap_inline4669#<tex2html_image_mark>#tex2html_wrap_inline4670#<tex2html_image_mark>#tex2html_wrap_inline4671#<I>by</I>2<tex2html_image_mark>#tex2html_wrap_inline4672# = <tex2html_image_mark>#tex2html_wrap_inline4673#<tex2html_image_mark>#tex2html_wrap_inline4674#<tex2html_image_mark>#tex2html_wrap_inline4675#<I>by</I> - <tex2html_image_mark>#tex2html_wrap_inline4676#<tex2html_image_mark>#tex2html_wrap_inline4677#<tex2html_image_mark>#tex2html_wrap_inline4678#<I>by</I> - <tex2html_image_mark>#tex2html_wrap_inline4679#<tex2html_image_mark>#tex2html_wrap_inline4680#<tex2html_image_mark>#tex2html_wrap_inline4681#<I>by</I>5<tex2html_image_mark>#tex2html_wrap_inline4682#<tex2html_image_mark>#tex2html_wrap_inline4683#<I>by</I>1<tex2html_image_mark>#tex2html_wrap_inline4684#, for example.
(These are Hasse diagrams of state spaces, with <I>q</I><SUB>0</SUB> at the bottom.)
<P>
To show <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4687#</SUP> is a state space, let <I>Y</I> be <tex2html_verbatim_mark>#math184#<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4690#</SUP> - {<I>q</I><SUB>0</SUB>}. It
suffices to show that any nonempty subset <tex2html_verbatim_mark>#math185#<I>Z</I>⊆<I>Y</I> has a meet in
<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4693#</SUP>. Now if <I>Z</I> has no lower bound in <I>Y</I> then <I>q</I><SUB>0</SUB> is the meet
of <I>Z</I> in <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4699#</SUP>. Otherwise let <I>W</I> be the set of lower bounds on
<I>Z</I> in <I>Y</I>. In <I>A</I>, <I>Z</I> is a set of lower bounds on <I>W</I>, hence
<tex2html_verbatim_mark>#math186#<tex2html_image_mark>#tex2html_wrap_inline4707#<I>W</I> in <I>A</I> is an upper bound on <I>Z</I> in <I>A</I>, therefore not
equal to <I>q</I><SUB>0</SUB>, therefore the join of <I>W</I> in <I>Z</I>. This join is at once
a lower bound on <I>Z</I> and dominates <I>W</I>, hence it is the meet of <I>Z</I>.
<P>
We define the <#306#><I>converse</I><#306#> <tex2html_verbatim_mark>#math187#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4718# of a state space to be its order
dual, an event space. We define the <#307#><I>complement</I><#307#> <I>A</I><SUP>-</SUP> to be
<tex2html_verbatim_mark>#math188#<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4721#</SUP><tex2html_image_mark>#tex2html_wrap_inline4722#, the converse of the dual of <I>A</I>, an event space. The
complement can be obtained simply by removing the initial state <I>q</I><SUB>0</SUB>
and reinstalling it as the final event ∞. The complement of an
event space is the state space obtained via the inverse procedure:
move top to bottom.
<P>
The complement of a state space turns states into their corresponding
Static conjunction <I>A</I>∧<I>B</I> is product of state spaces viewed as
posets: form the cartesian product of their underlying sets and then
order <tex2html_verbatim_mark>#math195#(<I>x</I>, <I>y</I>)≤(<I>x'</I>, <I>y'</I>) just when <I>x</I>≤<I>x'</I> and <I>y</I>≤<I>y'</I>. It is
straightforward to verify that <I>A</I>∧<I>B</I> so defined is a state space.
Define <I>A</I>∨<I>B</I> by De Morgan's law to be <tex2html_verbatim_mark>#math196#(<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4853#</SUP>∧<I>B</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4854#</SUP>)<SUP><tex2html_image_mark>#tex2html_wrap_inline4855#</SUP>.
The one-state space serves as unit for both static connectives.
<P>
We write <tex2html_verbatim_mark>#math197#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4857#<tex2html_image_mark>#tex2html_wrap_inline4858#-9<I>mu</I><TT>o</TT><I>B</I> for the set of state maps from <I>A</I> to <I>B</I>. We
partially order <tex2html_verbatim_mark>#math198#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4862#<tex2html_image_mark>#tex2html_wrap_inline4863#-9<I>mu</I><TT>o</TT><I>B</I> pointwise: <I>f</I>≤<I>g</I> in <tex2html_verbatim_mark>#math199#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4866#<tex2html_image_mark>#tex2html_wrap_inline4867#-9<I>mu</I><TT>o</TT><I>B</I> just when
<tex2html_verbatim_mark>#math200#<I>f</I> (<I>x</I>)≤<I>g</I>(<I>x</I>) for all <I>x</I> in <I>A</I>. To see that <tex2html_verbatim_mark>#math201#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4872#<tex2html_image_mark>#tex2html_wrap_inline4873#-9<I>mu</I><TT>o</TT><I>B</I> is a state
space it suffices to show that the pointwise meet <tex2html_verbatim_mark>#math202#<tex2html_image_mark>#tex2html_wrap_inline4875#<I>Z</I> of
any nonempty set <I>Z</I> of maps in <tex2html_verbatim_mark>#math203#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4878#<tex2html_image_mark>#tex2html_wrap_inline4879#-9<I>mu</I><TT>o</TT><I>B</I> is a state map, accomplished
We define <tex2html_verbatim_mark>#math206#<I>A</I>⊗<I>B</I> = (<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4917#<tex2html_image_mark>#tex2html_wrap_inline4918#-9<I>mu</I><TT>o</TT><I>B</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4919#</SUP>)<SUP><tex2html_image_mark>#tex2html_wrap_inline4920#</SUP>, and define <tex2html_verbatim_mark>#math207#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4922#<I>emB</I>
by De Morgan's law to be <tex2html_verbatim_mark>#math208#(<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4924#</SUP>⊗<I>B</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4925#</SUP>)<SUP><tex2html_image_mark>#tex2html_wrap_inline4926#</SUP>. The 2-element
state space <tex2html_verbatim_mark>#math209#<tex2html_image_mark>#tex2html_wrap_inline4928# = 2<tex2html_image_mark>#tex2html_wrap_inline4929# = 1<tex2html_image_mark>#tex2html_wrap_inline4930# = <tex2html_image_mark>#tex2html_wrap_inline4931#<tex2html_image_mark>#tex2html_wrap_inline4932#<tex2html_image_mark>#tex2html_wrap_inline4933#<I>by</I>2<tex2html_image_mark>#tex2html_wrap_inline4934# = <tex2html_image_mark>#tex2html_wrap_inline4935#<tex2html_image_mark>#tex2html_wrap_inline4936#<tex2html_image_mark>#tex2html_wrap_inline4937#<I>by</I> - <tex2html_image_mark>#tex2html_wrap_inline4938#<tex2html_image_mark>#tex2html_wrap_inline4939#<tex2html_image_mark>#tex2html_wrap_inline4940#<I>by</I> - <tex2html_image_mark>#tex2html_wrap_inline4941#<tex2html_image_mark>#tex2html_wrap_inline4942#<tex2html_image_mark>#tex2html_wrap_inline4943#<I>by</I>5<tex2html_image_mark>#tex2html_wrap_inline4944#<tex2html_image_mark>#tex2html_wrap_inline4945#<I>by</I>1<tex2html_image_mark>#tex2html_wrap_inline4946# serves as the common unit for both dynamic connectives.
<P>
We now define !<I>A</I>. An order filter <I>Y</I> of <I>A</I> is an upward-closed
subset of <I>A</I>, one such that if <I>x</I>≤<I>y</I> then <I>x</I>∈<I>Y</I> implies <I>y</I>∈<I>Y</I>. The order filters on <I>A</I> ordered by inclusion form a complete
lattice and hence a state space, the dual of which we define to be
!<I>A</I>. Those elements of !<I>A</I> (construed as order filters of <I>A</I>)
maximal in !<I>A</I> with respect to containing a given element <I>x</I> of <I>A</I>
form a poset isomorphic to the underlying poset <I>U</I>(<I>A</I>) of <I>A</I>.
<P>
We call !<I>A</I> the <#322#><I>free state space on</I><#322#> <I>U</I>(<I>A</I>). !<I>A</I> has the
property that for any state space <I>B</I>, the state maps from !<I>A</I> to <I>B</I>,
when restricted to <I>A</I>, are exactly the poset (i.e. monotone) maps from
<I>U</I>(<I>A</I>) to <I>U</I>(<I>B</I>). Thus whereas <tex2html_verbatim_mark>#math210#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4973#<tex2html_image_mark>#tex2html_wrap_inline4974#-9<I>mu</I><TT>o</TT><I>B</I> is the state space of all
state maps from <I>A</I> to <I>B</I>, <tex2html_verbatim_mark>#math211#!<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4978#<tex2html_image_mark>#tex2html_wrap_inline4979#-9<I>mu</I><TT>o</TT><I>B</I> is the larger state space of
all poset maps from <I>A</I> to <I>B</I>. The effect of ! has been to strip
off the structure of <I>A</I> to permit a clearer view, as discussed earlier
and again below in the section on measurement.
<P>
Then ?<I>A</I> is <tex2html_verbatim_mark>#math212#(!(<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline4986#</SUP>))<SUP><tex2html_image_mark>#tex2html_wrap_inline4987#</SUP>, and <tex2html_verbatim_mark>#math213#<I>A</I>⇒<I>B</I> is <tex2html_verbatim_mark>#math214#!<I>A</I><tex2html_image_mark>#tex2html_wrap_inline4990#<tex2html_image_mark>#tex2html_wrap_inline4991#-9<I>mu</I><TT>o</TT><I>B</I>, as
usual.
<P>
startsection <#1145#>subsection<#1145#><#1146#>2<#1146#><#1147#>@<#1147#><#1148#>12pt plus 2pt minus 2pt<#1148#>
<#1149#>12pt plus 2pt minus 2pt<#1149#><#1150#>setsizesubsize<#1151#>12pt<#1151#>xipt<B></B><#1150#><#323#>Behavioral Interpretation<#323#>
<P>
The state space interpretations of the connectives of linear logic
suggest natural behavioral interpretations.
<P>
We give the state space perspective for the static operations, then
pass to event spaces for the rest. The meaning of any connective in
state spaces is just the De Morgan dual of the corresponding connective
for event spaces and vice versa.
<P>
Recall that we defined <I>A</I>∧<I>B</I> as cartesian product: this
corresponds to the usual definition from automata theory of the
concurrent automaton <I>A</I><tex2html_image_mark>#tex2html_wrap_inline4994#<I>B</I> (the automaton interleaving the traces
of <I>A</I> and <I>B</I>) as the product of the two automata, with each
transition from (<I>a</I>, <I>b</I>) to (<I>a'</I>, <I>b</I>) corresponding to a transition of
<I>A</I> and from (<I>a</I>, <I>b</I>) to (<I>a</I>, <I>b'</I>) a transition of <I>B</I>. We illustrate
this with the example of two one-transition automata running
We call this <#328#><I>mingle</I><#328#>, but we do not have a simple familiar example
of it. The common unit of both connectives is <tex2html_verbatim_mark>#math223#<tex2html_image_mark>#tex2html_wrap_inline5369# = 2<tex2html_image_mark>#tex2html_wrap_inline5370# = 1<tex2html_image_mark>#tex2html_wrap_inline5371# = <tex2html_image_mark>#tex2html_wrap_inline5372#<tex2html_image_mark>#tex2html_wrap_inline5373#<tex2html_image_mark>#tex2html_wrap_inline5374#<I>by</I>2<tex2html_image_mark>#tex2html_wrap_inline5375# = <tex2html_image_mark>#tex2html_wrap_inline5376#<tex2html_image_mark>#tex2html_wrap_inline5377#<tex2html_image_mark>#tex2html_wrap_inline5378#<I>by</I> - <tex2html_image_mark>#tex2html_wrap_inline5379#<tex2html_image_mark>#tex2html_wrap_inline5380#<tex2html_image_mark>#tex2html_wrap_inline5381#<I>by</I> - <tex2html_image_mark>#tex2html_wrap_inline5382#<tex2html_image_mark>#tex2html_wrap_inline5383#<tex2html_image_mark>#tex2html_wrap_inline5384#<I>by</I>5<tex2html_image_mark>#tex2html_wrap_inline5385#<tex2html_image_mark>#tex2html_wrap_inline5386#<I>by</I>1<tex2html_image_mark>#tex2html_wrap_inline5387#.
<P>
The behavioral interpretation of the remaining connectives, still for
event spaces, all involve the notion of measurement. This can be read
either before or after the following section on measurement: each helps
to reinforce the other.
<P>
We read <tex2html_verbatim_mark>#math224#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline5389#<tex2html_image_mark>#tex2html_wrap_inline5390#-9<I>mu</I><TT>o</TT><I>B</I> as <I>A</I> <#329#><I>observed-by</I><#329#> <I>B</I>, illustrated by the
left equation in the diagram below. This is peer observation, thought
of as <I>B</I> unable to see <I>A</I> clearly due to <I>A</I>'s ``structure veil.''
In contrast <tex2html_verbatim_mark>#math226#!<I>A</I><tex2html_image_mark>#tex2html_wrap_inline5495#<tex2html_image_mark>#tex2html_wrap_inline5496#-9<I>mu</I><TT>o</TT><I>B</I> or <tex2html_verbatim_mark>#math227#<I>A</I>⇒<I>B</I> is <I>A</I> <#331#><I>diagnosed-by</I><#331#> <I>B</I>:
<I>B</I> observing <I>A</I> rendered transparent by !, as illustrated by the
equation on the right in the diagram above. Here !<I>A</I> is the <#332#><I>skeleton</I><#332#> or underlying structure of <I>A</I>, put back in the physical
world in the form of the free event space on that underlying
structure: <tex2html_verbatim_mark>#math228#!<I>A</I> = <I>F</I>(<I>U</I>(<I>A</I>)). The idea of underlying structure comes
across much more clearly in this constructive model than in the
nonconstructive phase space model.
<P>
The identity <tex2html_verbatim_mark>#math229#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline5506#<tex2html_image_mark>#tex2html_wrap_inline5507#-9<I>mu</I><TT>o</TT>(<I>B</I><tex2html_image_mark>#tex2html_wrap_inline5508#<tex2html_image_mark>#tex2html_wrap_inline5509#-9<I>mu</I><TT>o</TT><I>C</I>)≅(<I>A</I>⊗<I>B</I>)<tex2html_image_mark>#tex2html_wrap_inline5510#<tex2html_image_mark>#tex2html_wrap_inline5511#-9<I>mu</I><TT>o</TT><I>C</I> identifies
``while observing <I>B</I>, <I>C</I> observes <I>A</I>'' with ``<I>C</I> observes <I>A</I>
flowing through <I>B</I>.'' So the effect of <I>A</I> drifting into <I>C</I>'s field
of view while observing <I>B</I> is for <I>A</I> to flow through <I>B</I> to put them
both in the field of view together, interacting strongly.
<P>
The identity <tex2html_verbatim_mark>#math230#<I>A</I><tex2html_image_mark>#tex2html_wrap_inline5524#<tex2html_image_mark>#tex2html_wrap_inline5525#-9<I>mu</I><TT>o</TT><I>B</I>≅<I>B</I><SUP><tex2html_image_mark>#tex2html_wrap_inline5526#</SUP><tex2html_image_mark>#tex2html_wrap_inline5527#<tex2html_image_mark>#tex2html_wrap_inline5528#-9<I>mu</I><TT>o</TT><I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline5529#</SUP> might be the equivalence
of <I>B</I>'s acquiring position information from <I>A</I> with <I>A</I>'s acquiring
momentum from <I>B</I>.
<P>
The identity <tex2html_verbatim_mark>#math231#<I>A</I>⇒(<I>B</I>⇒<I>C</I>)≅(<I>A</I>∧<I>B</I>)⇒<I>C</I> illustrates the
difference superiority makes in observing. ``While diagnosing <I>B</I>, <I>C</I>
diagnoses <I>A</I>'' is equivalent to ``<I>C</I> diagnoses one of <I>A</I> or <I>B</I>.''
With <tex2html_verbatim_mark>#math232#<tex2html_image_mark>#tex2html_wrap_inline5542#<tex2html_image_mark>#tex2html_wrap_inline5543#-9<I>mu</I><TT>o</TT>, the observer had to settle for observing an intimate
mixing of the two objects, making it hard to resolve them. With <tex2html_verbatim_mark>#math233#⇒
the observer has no difficulty distinguishing <I>A</I> from <I>B</I> and gets to
choose which of <I>A</I> or <I>B</I> to diagnose. Noting that <tex2html_verbatim_mark>#math234#(<I>A</I>∧<I>B</I>)⇒<I>C</I>≅!(<I>A</I>∧<I>B</I>)<tex2html_image_mark>#tex2html_wrap_inline5550#<tex2html_image_mark>#tex2html_wrap_inline5551#-9<I>mu</I><TT>o</TT><I>C</I>≅(!<I>A</I>⊗!<I>B</I>)<tex2html_image_mark>#tex2html_wrap_inline5552#<tex2html_image_mark>#tex2html_wrap_inline5553#-9<I>mu</I><TT>o</TT><I>C</I>, we may think of ! as
freezing <I>A</I> and <I>B</I> before running them together; in their frozen
state they do not mix, making it easier for <I>C</I> not only to tell them
apart but to choose which to observe.
<P>
startsection <#1562#>section<#1562#><#1563#>1<#1563#><#1564#>@<#1564#><#1565#>24pt plus 2pt minus 2pt<#1565#>
<#1566#>12pt plus 2pt minus 2pt<#1566#><#1567#><FONT SIZE="+1"><B></B></FONT><#1567#><#333#>Measurement<#333#>
<P>
We now draw attention to a feature of a generalization of the linear
automaton model, namely a naturally arising Heisenberg uncertainty
principle. Such a principle is usually associated with the Fourier
transform, which transforms a sharply defined value in one domain,
represented by a delta function, to a diffuse spread of values in the
complementary domain. Our analysis finds this uncertainty in a wider
range of phenomena, the essential common feature of which is duality.
The Fourier transform is associated with Pontrjagin duality, but one
can also find signs of it in Stone duality and other dualities, as we
shall do here.
<P>
By ``certainty'' we have in mind precision, which we correlate with
variety of possible measurements. A certainty or precision of <I>n</I> bits
corresponds to having 2<SUP>n</SUP> possible measurements; conversely the
existence of <I>m</I> distinguishable measurements is associated with a
precision of log<SUB>2</SUB><I>m</I> bits.
<P>
We define a <#334#><I>measurement</I><#334#> to be a function <I>f</I> : <I>A</I>→<I>B</I> where <I>A</I> is
the measured object and <I>B</I> the measurement alphabet. For example <I>A</I>
may be the set of pixels on your computer screen, <I>B</I> the set of
possible colors of each pixel, and <I>f</I> : <I>A</I>→<I>B</I> one of the | <I>B</I>|<SUP>| A|</SUP>
possible screen images, <tex2html_verbatim_mark>#math235#2<SUP>2<SUP>20</SUP></SUP> in the case of a monochrome
1K×1K screen.
<P>
Such a screen is specified to a precision of 2<SUP>20</SUP> bits, one bit per
pixel. If | <I>B</I>| = 256, corresponding to 8 bits per pixel, the precision
would become 2<SUP>23</SUP> bits.
<P>
But now suppose that for some reason not every screen can occur, for
example if every white pixel is required to have at least four white
pixels touching it along an edge or at a corner. The precision then
drops, that is, uncertainty increases.
<P>
A natural kind of restricted function is the <#339#><I>homomorphism.</I><#339#> This
is a function between two similar algebras, e.g. two groups, that
etc. For example there are four functions from the two-element group
<I>C</I><SUB>2</SUB> to itself, only two of which are group homomorphisms.
<P>
In this last example, the passage from functions to group homomorphisms
is associated with an increase of one bit in uncertainty. It is as
though the effect of group structure were a veil hiding part of the
group.
<P>
State spaces and their dual event spaces are too small a class to
exhibit more than the special case of Heisenberg uncertainty, where
both the automaton and its dual appear equally uncertain. In a
separate paper we will describe a uniform generalization of state and
event spaces to a single category PDL of partial distributive
lattices. Informally a PDL is a distributive lattice where any given
meet or join may or may not be defined. Maps of such preserve those
meets and joins that exist. This provides a uniform framework
embedding both state and event spaces in the one category, along with
other structures such as sets, posets, semilattices, complete
semilattices, distributive lattices, and Boolean algebras. A state
space has all nonempty meets and the empty join, and no nonempty joins
or the empty meet. An event space has the exact opposite. A set has
no meets or joins save the trivial one-element ones:
<tex2html_verbatim_mark>#math238#<tex2html_image_mark>#tex2html_wrap_inline5577#{<I>x</I>} = <tex2html_image_mark>#tex2html_wrap_inline5578#{<I>x</I>} = <I>x</I>. At the other extreme a complete
atomic Boolean algebra (CABA) has all meets and joins.
<P>
The original motivation for this extension was to accommodate behaviors
that are recognized by the concurrency community as important but that
state spaces cannot represent. PDL's turn out to have a natural
characterization as a programming language of all monotone Boolean
operations.
<P>
Let us first consider sets and CABA's. We interpret a set as a
schedule having no structure, i.e. no veil, with every event clearly
distinguishable and constituting an independent primitive event. Call
this the <#342#><I>discrete</I><#342#> or <#343#><I>purely conjunctive</I><#343#> schedule, all of
whose events must happen. When we observe such a schedule to see which
events have happened so far it is possible to obtain any of the 2<SUP>n</SUP>
possible outcomes. Thus we associate <I>n</I> bits of observable
information with the <I>n</I>-event discrete schedule.
<P>
The dual of an <I>n</I>-element set is an <I>n</I>-atom CABA. As with any PDL we
can view it as either a schedule or an automaton (not with the same
behavior however). Viewed as an automaton this is just the automaton
complementary to our purely conjunctive schedule but with time
reversed, corrected by taking its converse (recall that complement is
composition of converse with dual, <tex2html_verbatim_mark>#math239#<I>A</I><SUP>-</SUP> = <I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline5585#</SUP><tex2html_image_mark>#tex2html_wrap_inline5586#).
<P>
There are only <I>n</I> Boolean algebra homomorphisms from it to the
2-element CABA preserving all meets and joins, namely the <I>n</I>
projections onto one of the <I>n</I> dimension. This corresponds to
choosing exactly one state, as an event. Furthermore, ordered
pointwise, the set of these events is discretely ordered, showing that
we have faithfully recovered the dual event space (so the uncertainty
of the complement of an object can be determined directly from the
object's cardinality).
<P>
We thus see that there are <I>n</I> bits of information visible in the
discrete schedule but only <tex2html_verbatim_mark>#math240#log<SUB>2</SUB><I>log</I><SUB>2</SUB><I>N</I> bits visible in the <I>N</I>-state
automaton dual to it. This is as indistinct as any <I>N</I>-state automaton
can get.
<P>
The same calculations show that the <I>N</I>-element CABA, as a schedule, is
a maximally veiled schedule, and its complementary automaton is
perfectly focused. This is the <#344#><I>purely disjunctive</I><#344#> behavior:
choose a state and stay there, the automaton having no transitions.
<P>
As sets start to acquire meets or joins, their dual Boolean algebras
concomitantly lose meets and joins. This corresponds to the ``veil''
gradually shifting from the CABA side to the set side. Event and state
spaces are in the exact middle of this tradeoff: every schedule has the
cardinality of its complementary automaton, hence two such
complementary <I>N</I>-element views of behavior share their <I>log</I><SUB>2</SUB><I>N</I> bits
equally between them. The Fourier analysis equivalent of this symmetry
is obtained for white noise, where both the signal and its dual
spectrum are (approximately?) normally distributed.
<P>
Chains (linear orders) represent rigid (no branching) local (no
concurrency) behavior and form a natural subcategory of event spaces
where the triumvirate of duality, complementarity, and converse can be
studied closely yet painlessly [#Pr92e#<tex2html_cite_mark>#1##<tex2html_cite_mark>#]. An <I>n</I>-event linear
schedule is quite indistinct, having only <I>log</I><SUB>2</SUB><I>n</I> bits, as does its
complementary (<I>n</I>±1)-state linear automaton (the ±1 depending on
which bounds are coded in the schedule). In effect all we can observe
of a sequential schedule is which transition between two events we are
presently in, the rest of the schedule before and after is invisible to
mortals.
<P>
The role of !<I>A</I> in these models of behavior is, as we said, to pull
the structure veil aside to reveal the inner workings (underlying
poset) of <I>A</I>, permitting a greater variety of measurements (more
precision of observation) than with the veil in place. If !<I>A</I> is
chosen to be the underlying poset then for chains with say a top we
gain only one additional observation, the one that does not preserve
that top. Hence this !<I>A</I> for chains does not clarify the view
appreciably.
<P>
However by removing yet more structure, corresponding in this case to
having a different !<I>A</I> operation yielding the underlying <#346#><I>set</I><#346#>, we
can then see the whole linear schedule in sharp relief. This
illustrates that structure need not be monolithic: the doctor can
undress you for a first examination, then use the X-ray machine to see
through your skin to obtain even sharper detail.
<P>
Since <tex2html_image_mark>#tex2html_wrap_inline5607# is discrete (two elements), Planck's constant <tex2html_image_mark>#tex2html_wrap_inline5609# has
not entered. If it had, we would construe !<I>A</I> as shrinking <tex2html_image_mark>#tex2html_wrap_inline5612#
(locally to <I>A</I>) to zero to make <I>A</I> behave classically.
<P>
startsection <#1569#>section<#1569#><#1570#>1<#1570#><#1571#>@<#1571#><#1572#>24pt plus 2pt minus 2pt<#1572#>
<#1573#>12pt plus 2pt minus 2pt<#1573#><#1574#><FONT SIZE="+1"><B></B></FONT><#1574#><#347#>Conclusion<#347#>
<P>
We have extended Birkhoff and von Neumann's propositional quantum logic
of uncertain states to a logic of the duality of time and information.
Its joint programming language and verification logic is linear logic.
More behavioral phenomena are captured by this linear logic of behavior
than by quantum logic alone. On the other hand the extension is not
faithful to the orthodox view of quantum mechanical dynamics, and we
raise as an open problem how to formulate the dynamic quantum logic of
standard quantum mechanics.
<P>
One might ask why the well-behaved static implication <tex2html_verbatim_mark>#math241#<I>A</I>⇒<I>B</I> of
linear logic had not previously been found for quantum logic. The
answer seems to hinge on the need for static implication to refer to
the dynamic part, <tex2html_verbatim_mark>#math242#<I>A</I>⇒<I>B</I>~ = ~!<I>A</I><tex2html_image_mark>#tex2html_wrap_inline5617#<tex2html_image_mark>#tex2html_wrap_inline5618#-9<I>mu</I><TT>o</TT><I>B</I>, even when static conjunction
does not. That negation is obtained via dynamic implication,
<tex2html_verbatim_mark>#math243#<I>A</I><SUP><tex2html_image_mark>#tex2html_wrap_inline5620#</SUP> = <I>A</I><tex2html_image_mark>#tex2html_wrap_inline5621#<tex2html_image_mark>#tex2html_wrap_inline5622#-9<I>mu</I><TT>o</TT><tex2html_image_mark>#tex2html_wrap_inline5623#, and static disjunction is in turn obtained as the
De Morgan dual of static conjunction via that negation, indicates that
these too are tied to the dynamic part. This suggests that the root of
quantum logic's implication problem might lie with not bringing time
into the logic.
<P>
<#348#><I>Acknowledgement.</I><#348#> I am very grateful to John Baez for his